ProCoS
Kontakt
Leitung
Sekretariat
Contact
Head
Secretary
ProCoS
Transformational development of reactive systems
Project duration: 1 October 1989 to 30 September 1999
Financing by: University and DFG
Reactive systems provide certain services through constant interaction with their environment. The aim of transformational development is to systematically create correct software for such systems from specifications using transformation rules. Work on this topic began in the Semantics Department as part of the ESPRIT basic project ProCoS (Provably Correct Systems, 1989-95). We are focussing on reactive systems consisting of parallel components that can exchange messages with each other by means of synchronous communication.
For these communicating systems a specification language SL was developed and a programming language PL similar to OCCAM was considered. The transformations developed in the ProCoS project work on a language MIX of so-called mixed terms that mix specification and programme operators. A state trace readiness model for communicating systems served as the semantic basis.
During the reporting period, J. Bohn completed a formalisation and implementation of the MIX approach in the theorem prover LAMBDA in his dissertation. The implementation also includes tactics for semi-automatic programme synthesis from specifications.
M. Schenke extended the MIX approach in his habilitation thesis in such a way that time-critical systems can also be handled. The starting point are real-time requirements, which are specified in a subset of the duration calculus. Using novel transformations, these requirements can first be transformed into specifications from SL-time, a real-time extension of SL, and from there into OCCAM-like programmes with time constructs.
Graphical specification of requirements
Project duration: 1.10.1994 to 30.9.1999
Financing by: University and DFG
When formalising requirements for systems to be constructed, experts from the respective application area meet experts from Computing Science. It is therefore necessary to find specification languages that both groups understand. Graphical specification formalisms are one approach to this. While graphical approaches for describing transition systems have been known for a long time (automata, Petri nets, state charts), graphical descriptions of requirements for the behaviour of systems are still in an experimental phase. Well-known examples are Message Sequence Charts (MSCs) and the Symbolic Timing Diagrams developed in the department of W. Damm.
In the Semantics department, C. Dietz has developed a new graphical specification formalism for real-time requirements, called constraint diagrams. These diagrams are motivated by the Symbolic Timing Diagrams, but differ in their semantics. This is described on the basis of the Duration Calculus in the so-called Assumption-Commitment style. This ensures a connection to further work of the department on the basis of the Duration Calculus.