On the Verification of Formal Methods for Digital Embedded Control Systems | Consortium for Embedded Systems | SIU

Abstract: Specifications and requirements for embedded control systems need typically to be modelled at a higher level than that of the implementation for several reasons: (i) specifications and requirements are constantly changed/refined at least in the initial design phases; (ii) conflicts/incompatibilities in the design can be found at an earlier stage; (iii) descriptive and notational formalisms are needed so that reliability, performance and quality assurance standards are maintained throughout the design development. Several formal methods have been developed for this purpose, including the VDM and Z formal languages. Although these languages provide formal semantics that allow in principle the proof and verification of the properties of the model, they are not accompanied by adequate tools to support automatic verification. In this project, we propose to investigate existing approaches and develop new ones in order to aid the automatic verification/validation/consistency check of the requirements, as they are dynamically developed in the design modelling process of digital embedded control systems.

Problem: Formal design specification methods like the VDM and Z formal languages allow in principle the proof and verification of the properties of the design model, but existing tools for automatic proof (like the PVS and Isabelle-based theorem provers) are not adequate and/or are not addressing the specific needs of specific digital embedded control systems.

Rationale / Approach: Identifying the specific needs of an embedded control system and customizing an automatic proof method that can be used in each particular case is a promising way to provide the much needed verification/validation/consistency check. Given a formal specification of requirements of a digital embedded control system in a formal language such as VDM, we will investigate how well the requirements can be modeled and verified/validated using the powerful Satisfiability Module Theories (SMT) and Boolean Satisfiability (SAT) methods. Trade-offs in applicability and computation complexity will also be investigated.

Novelty: Existing tools for automatic proof (like the PVS and Isabelle-based theorem provers) are not adequate and/or are not addressing the specific needs of specific digital embedded control systems for formal verification. This project will provide methodologies and results on specific industrial cases.

Potential Member Company Benefits: Formal design specification is much in demand and the present study will provide additional insight in the automatic verification process.
Deliverables for the proposed year: The deliverables for this project are (1) a methodology for automatic verification/validation/consistency check of formal requirements and (2) application of the approach on an industrial case studies.

Milestones for the proposed year: Quarters 1 and 2: Exploration of the capabilities of existing theorem provers/SAT solvers that can work in conjunction with Formal Methods. Quarters 3 and 4: Development and application of SMT/SAT based method and application to industrial cases.