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.