Evaluating Context Descriptions and Property Definition Patterns for Software Formal Validation - ENSTA Bretagne - École nationale supérieure de techniques avancées Bretagne Accéder directement au contenu
Communication Dans Un Congrès Année : 2011

Evaluating Context Descriptions and Property Definition Patterns for Software Formal Validation

Résumé

A well known challenge in the formal methods domain is to improve their integration with practical engineering methods. In the context of embedded systems, model checking requires first to model the system to be validated, then to formalize the properties to be satisfied, and finally to describe the behavior of the environment. This last point which we name as the proof context is often neglected. It could, however, be of great importance in order to reduce the complexity of the proof. The question is then how to formalize such a proof context. In the Topcased project, we designed a language, named CDL (Context Description Language), for describing a system environment using actors and sequence diagrams, together with the properties to be checked. The properties are specified with textual patterns and attached to specific regions in the context. CDL is designed so that formal artifacts required by existing model checkers could be automatically generated from it. This generation is currently implemented in a prototype tool named OBP (Observer Based Prover). Our contribution is a report on several industrial embedded system applications and our future works.
Fichier non déposé

Dates et versions

hal-00635653 , version 1 (25-10-2011)

Identifiants

  • HAL Id : hal-00635653 , version 1

Citer

Philippe Dhaussy, Frédéric Boniol, Pierre-Yves Pillain, Xavier Dumas. Evaluating Context Descriptions and Property Definition Patterns for Software Formal Validation. Topcased days, Feb 2011, Toulouse, France. ⟨hal-00635653⟩
200 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More