Verification and Code Generation for Timed Transitions in pCharts. Nokovic, B. & Sekerinski, E. In C3S2E '14: Proceedings of the 2014 International C* Conference on Computer Science & Software Engineering, pages 3:1–3:10, August, 2014. ACM.
doi  abstract   bibtex   1 download  
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.
@inproceedings{NokovicSekerinski14TimedpCharts,
	title = {Verification and {Code} {Generation} for {Timed} {Transitions} in {pCharts}},
	doi = {10.1145/2641483.2641522},
	abstract = {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.},
	booktitle = {{C3S2E} '14: {Proceedings} of the 2014 {International} {C}* {Conference} on {Computer} {Science} \& {Software} {Engineering}},
	publisher = {ACM},
	author = {Nokovic, Bojan and Sekerinski, Emil},
	editor = {Desai, Bipin C.},
	month = aug,
	year = {2014},
	pages = {3:1--3:10},
}

Downloads: 1