«

»

Evaluating Context Descriptions and Property Definition Patterns for Software Formal Validation

by Philippe Dhaussy, Pierre Yves Pillain, Stephen Creff, Amine Raji, Yves Le Traon, Benoit Baudry
Abstract:
Formal methods need better integration with engineering practices. In the context of embedded systems, model checking requires first to model the component to be verified, then to formalize the properties to be satisfied and finally to describe the behavior of the environment. The proof context, which is a model of the environment behavior, is in practice often neglected. It is, however, of great importance in order to reduce the complexity of the proof. The question is to formalize such a proof context. We are experimenting a DSL, named Context Description Language (CDL), which describes a software component environment using actors and sequence diagrams, together with the properties to be checked. The properties are specified with patterns, formulated textually and attached to specific regions of the context. CDL models are translated into timed automata which feed model checkers. Properties of the model are, as a result, checked automatically. The contribution of the paper is a report on the experiments applied on several industrial embedded system applications provided by the aviation, space and military areas.
Reference:
Evaluating Context Descriptions and Property Definition Patterns for Software Formal Validation (Philippe Dhaussy, Pierre Yves Pillain, Stephen Creff, Amine Raji, Yves Le Traon, Benoit Baudry), In Proceedings of the International Conference on Model Driven Engineering Languages and Systems (MODELS), 2009.
Bibtex Entry:
@inproceedings{dhaussy09,
	Abstract = {Formal methods need better integration with engineering practices.
	In the context of embedded systems, model checking requires first
	to model the component to be verified, then to formalize the properties
	to be satisfied and finally to describe the behavior of the environment.
	The proof context, which is a model of the environment behavior,
	is in practice often neglected. It is, however, of great importance
	in order to reduce the complexity of the proof. The question is to
	formalize such a proof context. We are experimenting a DSL, named
	Context Description Language (CDL), which describes a software component
	environment using actors and sequence diagrams, together with the
	properties to be checked. The properties are specified with patterns,
	formulated textually and attached to specific regions of the context.
	CDL models are translated into timed automata which feed model checkers.
	Properties of the model are, as a result, checked automatically.
	The contribution of the paper is a report on the experiments applied
	on several industrial embedded system applications provided by the
	aviation, space and military areas.},
	keywords = {MDE, analysis},
	Author = {Philippe Dhaussy and Pierre Yves Pillain and Stephen Creff and Amine Raji and Yves Le Traon and Benoit Baudry},
	Booktitle = {Proceedings of the International Conference on Model Driven Engineering Languages and Systems (MODELS)},
	Month = {October},
	Pages = {438-452},
	Title = {Evaluating Context Descriptions and Property Definition Patterns for Software Formal Validation},
	Url = {http://www.irisa.fr/triskell/publis/2009/dhaussy09.pdf},
	X-Country = {US},
	X-International-Audience = {yes},
	X-Language = {EN},
	X-Proceedings = {yes},
	Year = {2009},
	x-abbrv = {MODELS},
}