Title
Applying atomicity and model decomposition to a space craft system in event-B
Abstract
Event-B is a formal method for modeling and verifying consistency of systems. In formal methods such as Event-B, refinement is the process of enriching or modifying an abstract model in a step-wise manner in order to manage the development of complex and large systems. To further alleviate the complexity of developing large systems, Event-B refinement can be augmented with two techniques, namely atomicity decomposition and model decomposition. Our main objective in this paper is to investigate and evaluate the application of these techniques when used in a refinement based development. These techniques have been applied to the formal development of a space craft system. The outcomes of this experimental work are presented as assessment results. The experience and assessment can form the basis for some guidelines in applying these techniques in future cases.
Year
Venue
Keywords
2011
NASA Formal Methods
formal method,event-b refinement,space craft system,abstract model,experimental work,future case,large system,formal development,assessment result,model decomposition,atomicity decomposition,space,refinement
Field
DocType
Volume
Atomicity,Craft,Computer science,Formal development,Theoretical computer science,Refinement,Formal methods,Model decomposition
Conference
6617
ISSN
Citations 
PageRank 
0302-9743
9
0.64
References 
Authors
11
3
Name
Order
Citations
PageRank
Asieh Salehi Fathabadi1488.14
Abdolbaghi Rezazadeh2547.78
Michael Butler31768104.74