Title: pState: A probabilistic statecharts translator
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/rew...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.Read More
Publication Year: 2013
Publication Date: 2013-06-01
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 7
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot