Linearization of ?CRL specifications
We describe a linearization algorithm for ?CRL processes, similar to the one described in  for a subset of the language called parallel pCRL. This algorithm finds its roots in formal language theory: the `grammar' defining a process is transformed into a variant of Greibach Normal Form. Next, any such form is further reduced to linear form, i.e., to an equation that resembles a right-linear, data-parametric grammar. From the other perspective, linear specifications in ?CRL resemble symbolicrepresentations of transition systems, that can be further transformed and analyzed by many of the existing tools and techniques. We aim at proving the correctness of this linearization algorithm. To this end we use an equivalence relation on recursive specifications in ?CRL that is model independent and does not involve an explicit notion of solution.
|Requirements/Specifications (acm D.2.1), Software/Program Verification (acm D.2.4), Formal Definitions and Theory (acm D.3.1), Language Constructs and Features (acm D.3.3), Semantics of Programming Languages (acm F.3.2), Expressions and Their Representation (acm I.1.1)|
|Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (msc 68Q10), Grammars and rewriting systems (msc 68Q42), Abstract data types; algebraic specification (msc 68Q65), Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (msc 68Q85)|
|Software Engineering [SEN]|
|Organisation||Specification and Analysis of Embedded Systems|
Usenko, Y.S. (2002). Linearization of ?CRL specifications. Software Engineering [SEN]. CWI.