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 difficult to use in practice as they require extreme formalism. In this project, we propose (i) to develop a supporting tool that can translate requirements specified in a more natural language to the formal input required by a theorem prover; (ii) to investigate the capabilities a specific publicly available theorem prover (Z3 of Microsoft Research) to verify/check for consistency the given requirements; (iii) to develop a new Binary Decision diagram (BDD) based approach to handle incrementally new requirements as they are dynamically developed in the design modeling process of digital embedded control systems, and (iv) compare the performance of the incremental approach to the static approach.

Problem: Formal design specification methods like the VDM formal language allow in principle the proof and verification of the properties of the design model, but existing tools for automatic proof do not provide a “natural” way for engineers to specify their requirements in practice and/or are not addressing the specific needs of digital embedded control systems, like the incremental addition/revision of requirements.

Rationale / Approach: we propose to develop a tool that can translate from a “semi-formal” description of requirements to the extremely formal description that a theorem prover/solver needs. In addition, the requirements are constantly changed/revised during project development. Therefore, the benefits of an incremental approach over the standard approach of checking all requirements again from scratch is worth investigating.

Novelty: We propose a tool that can translate from a “semi-formal” description of requirements to the extremely formal description that a theorem prover/solver (specifically Z3) needs. We also investigate the incremental approach in requirements checking.

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 ar: (1) tool for translation of requirements form natural-language to formal specification. (2) Application of Z3 and investigation of its capabilities on an industrial case studies. (3) Investigation of the incremental approach in requirements checking

Milestones for the proposed year: Quarters 1 and 2: Translation tool. Quarters 3 and 4: Implementation and investigation of the incremental approach.