Combining Theorem Proving and Continuous Models in Synchronous Design

Support for system speci cation in terms of modelling and simulation environments has become a common practice in safety-critical applications. Also, a current trend is the automatic code-generation, and integration with formal methods tools in terms of translators from a high level design often using common intermediate languages. What is missing from current formal methods tools is a well-founded integration of models for di erent parts of a system, being software hardware or control-intensive data-intensive. By hardware we mean here the full range of domains in engineering systems including mechanics, hydraulics, electronics. Thus, there is a methodological gap for proving system properties from semantically well-de ned descriptions of the parts. We report on the progress achieved with the European SYRF project with regard to veri cation of integrated analog discrete systems. The project pursues the development of new theories, application to case studies, and tool development in pa...

• Type: Conference
• Year: 1999
• Where: FM
• Authors: Simin Nadjm-Tehrani, Ove Åkerlund
• Keywords: Common Intermediate Languages, Current Formal Methods, FM 1999, Formal Methods, Formal Methods Tools