Generating Processes from Specifications using the Relation Manipulation System RelView
Michael Winter · Electronic Notes in Theoretical Computer Science · 2003
In this paper we present an algorithm generating a bundle of processes from a given safety specification. The specification is given by a formula in a process logic, i.e. a modal logic with a set of possibility operators induced by the possible actions of the underlying transition system. This logic is a finite sublanguage, in the sense that only finite conjunctions are allowed, of the language introduced by R. Milner in [3]. Furthermore, we present an implementation of the algorithm using the functional language HASKELL and the internal language of the RelView system. Within the system processes are modelled by relations as shown in [8,9].