Some adjustments seem desirable for the following tasks. They result either from wrong guessing in the scientific objectives, or from unexpected research development, or from manpower availability problems.
During SYRF's first year of operation, a Lustre interface to the workbench was developed, i.e., a translator tool from Lustre to NP-Tools. Some limitations in the current version of the translator have been identified. Therefore, the workbench interface from the synchronous languages (an interface also from Esterel is planned) needs some more effort during SYRF's second year of operation.
Development of higher-level support for expressing requirements and properties of synchronous systems lost some momentum when key people left NP Technology in 1997, but this is currently activated again.
The improvements made to the Stålmarck method, merging the propagation and assumption rules of the method with constraint solving on the one hand, and adding stronger rules in conjunction with a relaxation of the subformula principle on the other, has been an interesting track which we believe should be continued.
We propose to reduce the planned activity of verification of asynchronous systems in favor of pursuing the above desribed tracks instead: further improvement of the Stålmarck method, improvements of workbench interfaces and a higher-level specification language.
One of Inria-EpAtr original objectives was to develop a library of real-time kernel components, written in Signal or DC+, to serve as a basis for building target architecture models. This work was planed early in the project. However it actually needs more experience than we currently have concerning concrete examples of distributed target architectures. Thus, we have decided to postpone, maybe significantly, this particular work.
In contrast, unexpected fundamental progresses have been made in a different, but related, direction, namely in providing a complete formal study of what "desynchronizing synchronous programs" means. This has been achieved by establishing a formal link between program compositions according to the synchronous paradigm, versus the asynchronous paradigm of partial order models. It is an important result as it will serve as a support for our distributed code generation technology. This work is currently under writing and will be available for the next review.
During this first year, we have been investigating the mapping from strong synchrony to true concurrency, and back -- a question related, but not identical, to the previous one. We have found what "desynchronization" means, and how true concurrent systems can be made synchronous. Although some results have been obtained while investigating this, the whole is somewhat disappointing as it looks somewhat trivial afterwards.
Meanwhile, in the process of investigating this area, we have developed a new conceptual tool, based on so-called MaxPlus algebraic techniques, which revealed being much more interesting than the original objective, and is still very relevant to the general objectives of SYRF. This is why we have chosen to provide this as a delivery for task 5.2.1, instead of our originally expected results.
The definition of methods for deriving discrete models of the plant from continuous models is still in progress and the corresponding results will be included in deliverable 7.2. Connection to abstract interpretations will be used to show the sufficiency for proving safety properties.
The documentation of the case study earlier promised under year 2 has instead started under year 1, and is partially presented as annex 1 to deliverable 7.1. The reason is the interest of the project partners to start with case studies earlier.