Verification and Code Generation for Timed Transitions in pCharts

This paper describes timed transition in pCharts, a variation of statecharts extended with probabilistic transitions, costs/rewards, and state invariants. Timed transitions with nondeterministic and stochastic timing can be used for the specification and analysis of real-time systems. We present a translation scheme for timed transition of pCharts into probabilistic timed automata (PTA) and executable C code, as implemented in our tool pState. To illustrate the development process, we analyze the power consumption of a radio-frequency identification (RFID) tag and generate code for the PIC micro-controller.