Incremental description of Systems based on the Calculus of Refinements and Executable Modal Logics:
Applications to Safety Critical Systems

CICYT Project TIC94-0847-C02-02


The research conducting to the development of correct and reliable software for Temporal Databases, Safety Critical Systems and Multiagent Systems is becoming increasingly important from both a scientific and an industrial point of view. Large commercial systems for software management already exist but these lack a rigourous formal semantics and are therefore likely to be limited in scale and reliability. On the other hand, formal systems for requirements specification exist but these have been applied only to small problems or to limited portions of the specification task. In this project we believe that the time is now ripe to apply techniques from computational logic to realistic sized specfication problems like the Safety Critical ones.

In subproject 1 we view the task of specification as a process of refinement between several level of detail of system description. Once the specification is sufficiently detailed it should be possible to test its behaviour by allowing to be executed in a controled way. If, after testing, a user is satisfied, it can be refined introducing new information, checking its coherence with the previous one. Once complete it should be possible to provide guidance in transforming the specification to code which may be executed more efficiently. The methodology is based on the language COR, a basic specification language easy to understand to extend following the needs of the user.

In the second subproject, we face the problem of designing knowledge representation languages adapted to the prolem domain. Because the applications to develop require reasoning about knowledge, time and believe, the languages to be used must be based on modal and temporal logic. Then our research focuses on the design of executable fragments of these logics using well known techniques.