Validation of COSMOS DSL programs

Author

MATOUGUI, Mohammed El Amine ; Leriche, Sébastien

Author_Institution

Inst. Telecom, Telecom SudParis, Évry, France

fYear

2010

fDate

Nov. 30 2010-Dec. 2 2010

Firstpage

307

Lastpage

313

Abstract

COSMOS DSL is a language dedicated to the domain of composition of context information. It allows, through its high-level constructions, to treat very large amounts of context data coming from distributed sources, whatsoever in ubiquitous systems or large-scale distributed systems. In this paper, we focus on the safety of programs developed in COSMOS DSL. We discuss the needs of reliability and validation of specific properties such as the lack of deadlocks and vivacity of context information. Then we propose an automatable modeling of COSMOS DSL using the Petri nets formalism to allow verification of behavioral properties in a software tool.

Keywords

Petri nets; formal verification; middleware; ubiquitous computing; COSMOS DSL language; Petri nets; behavioral property verification; context entities composition and sharing language; large-scale distributed systems; ubiquitous systems; Context; Context modeling; DSL; Observers; Petri nets; Synchronization; System recovery; Automatic validation; Petri nets; context-awareness; dedicated language; distributed systems;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Engineering and Systems (ICCES), 2010 International Conference on

Conference_Location

Cairo

Print_ISBN

978-1-4244-7040-2

Type

conf

DOI

10.1109/ICCES.2010.5674874

Filename

5674874