"ECOS: from formal specification to hardware/software partitioning"


Abstract:

We strongly believe that Co-Specification of Hw/Sw systems cannot be achieved
without Co-Operation of Hw/Sw teams: this work is developed via a dialectical
process between the Hw and the Sw teams of the LaMI.

The paper presents a first approach of the use of OO algebraic specifications
for Hw/Sw Co-Specification. Such a framework takes benefit of all the
usual advantages of formal methods: reliability of proof technics, automatic
treatment of the specification texts such as automatic test generation,
consistency checks and completeness issues. Moreover the OO paradigm allows
the building and the use of libraries, facilitates the reuse of already
specified objects, authorizes stepwise refinements and guides implementation
choices.

We take benefit of the most recent developments in the field of software
specification since OO algebraic specifications belong to the latest issues of
the European ESPRIT project ISCORE. In addition, we are in the process of
specifying the DLX RISC architecture using classical algebraic
specifications with exception handling capabilities.


Acknowledgements:

This work is partially supported by France-Telecom and the
French Ministry of research.