Anton Tarasyuk
Åbo Akademi University, Finland
Elena Troubitsyna
Åbo Akademi University, Finland
Linas Laibinis
Åbo Akademi University, Finland
Ladda ner artikel
Ingår i: NODES 09: NOrdic workshop and doctoral symposium on DEpendability and Security; Linköping; Sweden; April 27; 2009
Linköping Electronic Conference Proceedings 41:2, s. 11-20
Publicerad: 2009-07-14
ISBN:
ISSN: 1650-3686 (tryckt), 1650-3740 (online)
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.
Event-based modeling; reliability assessment; formal verification; Markov processes
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.
