Article | NODES 09: NOrdic workshop and doctoral symposium on DEpendability and Security; Linköping; Sweden; April 27; 2009 | Reliability Assessment in Event-B Development

Title:
Reliability Assessment in Event-B Development
Author:
Anton Tarasyuk: √Öbo Akademi University, Finland Elena Troubitsyna: √Öbo Akademi University, Finland Linas Laibinis: √Öbo Akademi University, Finland
Download:
Full text (pdf)
Year:
2009
Conference:
NODES 09: NOrdic workshop and doctoral symposium on DEpendability and Security; Linköping; Sweden; April 27; 2009
Issue:
041
Article no.:
002
Pages:
11-20
No. of pages:
10
Publication type:
Abstract and Fulltext
Published:
2009-07-14
Series:
Linköping Electronic Conference Proceedings
ISSN (print):
1650-3686
ISSN (online):
1650-3740
Publisher:
Linköping University Electronic Press; Linköpings universitet


Formal methods are indispensable for ensuring dependability of complex software-intensive systems. In particular; the B Method and its recent extension Event B have been successfully used in the development of several complex safety-critical systems. However; they are currently not supporting quantitative assessment of dependability attributes that is often required for certifying safetycritical systems.. In this paper we demonstrate by example how to integrate reliability assessment into Event B development. This work shows how to conduct probabilistic assessment of system reliability at the development stage rather than at the implementation level.

Keywords: Event-based modeling; reliability assessment; formal verification; Markov processes

NODES 09: NOrdic workshop and doctoral symposium on DEpendability and Security; Linköping; Sweden; April 27; 2009

Author:
Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis
Title:
Reliability Assessment in Event-B Development
References:

1. J.-R. Abrial. Extending B without changing it (for developing distributed systems). In H. Habiras editor; First Conference on the B method; pages 169-190. IRIN Institut de recherche en informatique de Nantes; 1996.


2. J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press; 2005.


3. RODIN Event-B Platform http://www.event-b.org/


4. E. W. Dijkstra. A Discipline of Programming. Prentice-Hall; 1976.


5. PRISM probabilistic model checker http://www.prismmodelchecker.org/


6. W. Feller. An Introduction to Probability Theory and Its Applications. John Wiley & Sons; 1967.


7. J. G. Kemeny; J. L. Snell. Finite Markov Chains. D. Van Nostrand Company; 1960.


8. D. J. White. Markov Decision Processes. John Wiley & Sons; 1993.


9. A. Villemeur. Reliability; Availability; Maintainability and Safety Assessment. John Wiley & Sons; 1991.


10. P. O’Connor. Practical Reliability Engineering. John Wiley & Sons; 1995.


11. A. K. McIver; C. C. Morgan; and E. Troubitsyna The probabilistic steam boiler: a case study in probabilistic data refinement. In J. Grundy; M. Schwenke; and T. Vickers; editors; Proc. International Refinement Workshop; ANU; Canberra; Discrete Mathematics and Computer Science; pages 250-265. Springer-Verlag; 1998.


12. A. K. McIver; C. C. Morgan. Abstraction; Refinement and Proof for Probabilistic Systems. Springer; 2005.

NODES 09: NOrdic workshop and doctoral symposium on DEpendability and Security; Linköping; Sweden; April 27; 2009

Author:
Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis
Title:
Reliability Assessment in Event-B Development
Note: the following are taken directly from CrossRef
Citations:
No citations available at the moment