pState: A probabilistic statecharts translator

Author

Nokovic, Bojan ; Sekerinski, Emil

Author_Institution

Comput. & Software Dept., McMaster Univ., Hamilton, ON, Canada

fYear

2013

fDate

15-20 June 2013

Firstpage

29

Lastpage

32

Abstract

We describe pState, an experimental software toolkit for the design, validation and formal verification of complex systems. Classical statecharts are extended with probabilistic transitions, costs/rewards, and state invariants. Probabilistic choice can be used to model randomized algorithms or unreliable systems. Costs/rewards can be used to compute quantitative properties such as expected power consumption or expected number of lost messages in model of some communication protocol. State invariants are used to express safety conditions or consistency constraints. The charts are validated and transformed into an intermediate representation, from which code for various languages can be generated.

Keywords

large-scale systems; probability; program interpreters; program verification; communication protocol; complex systems; consistency constraints; costs-rewards; experimental software toolkit; formal verification; pState; power consumption; probabilistic statecharts translator; randomized algorithms; safety conditions; state invariants; Computational modeling; invariants; model-checking; quantitative properties; statecharts; verification;

fLanguage

English

Publisher

ieee

Conference_Titel

Embedded Computing (MECO), 2013 2nd Mediterranean Conference on

Conference_Location

Budva

ISSN

1800-993X

Type

conf

DOI

10.1109/MECO.2013.6601339

Filename

6601339