FORMAL VERIFICATION OF RECONFIGURABLE
funded by UEFISCDI under contract
|Domain||2. Information and communication technologies, space and security|
|Subdomain||2.1 Information and Communication Technologies
The field of formal specification and verification of software and
hardware systems is without alternative in safety-critical or security
areas where one cannot take the risk of failure. This includes several
success stories such as the verification of the Pentium IV arithmetic,
the verification of the Traffic Collision Avoidance System TCAS,
various security protocols, etc. In many cases, only the use of
logic-based techniques has been able to reveal serious bugs in software
and hardware systems; in other cases, spectacular and costly failures
such as the loss of the Mars Climate Orbiter could have been avoided by
formal techniques. Moreover it is well established that formal support
greatly enhances the efficiency of software development and maintenance.
An important class of software systems are the reconfigurable ones; these are software systems that behave differently in different modes of operation (often called configurations) and commute between them along their lifetime. Such systems, which evolve in response to external or internal stimulus, are everywhere: from e-Health or e-Government integrated services to sensor networks, from domestic appliances to complex systems distributed and collaborating over the web, from safety or mission-critical applications to massive parallel software.
The goal of this project is to develop an integrated formal specification and verification environment for reconfigurable systems that include a (1) dedicated generic logic-based specification language, (2) a formal verification tool, (3) a set of methodologies for using the specification and the verification tools and (4) a library of examples and case studies. The environment is meant to be used both as a working tool in industry and as educational tool in universities and research centers.
- Răzvan Diaconescu
- CS1, project director (Simion Stoilow Institute of Mathematics of the Romanian Academy – IMAR)
- Postodoctoral Researcher (Simion Stoilow Institute of Mathematics of the Romanian Academy – IMAR)
- Ultraproducts and possible worlds semantics in institutions, Theoretical Computer Science 379:210-230, Elsevier (2007)
- Encoding hybridized institutions into first order logic, Mathematical Structures in Computer Science 26:745-788, Cambridge University Press (2016)
- The Heterogeneous Tool Set, in O. Grumberg and M. Huth (Eds.): TACAS 2007, Lecture Notes in Computer Science 4424:519-522, Springer (2007).
- Scientific Report of the project for the period Aug. 2017 - Dec. 2017
- Scientific Report of the
project for 2018
Report of the project for the whole duration of the project
- visit of M. Codescu at the Hets group in Magdeburg, 30.10.2017 - 19.11.2017
- visit of R. Diaconescu at the Hets group in Magdeburg, 26.11.2017 - 9.12.2017
- The H system (including documentation, executables, libraries of examples and case study)