Techniques for the development of reliable information systems on the basis of their formal specification are the main concern in the project. Our work focuses on the specification language TROLL light which allows one to describe the part of the world to be modeled as a community of concurrently existing and communicating objects. Our specification language comes with an integrated, open development environment. The task of this environment is to give support for the creation of correct information systems. Two important ingredients of the environment are the animator and the proof support system.
展开▼