@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},
}

{"_id":"p2JHwntCwquQ8rvuE","bibbaseid":"nokovic-sekerinski-verificationandcodegenerationfortimedtransitionsinpcharts-2014","downloads":1,"creationDate":"2019-02-02T15:48:53.582Z","title":"Verification and Code Generation for Timed Transitions in pCharts","author_short":["Nokovic, B.","Sekerinski, E."],"year":2014,"bibtype":"inproceedings","biburl":"https://api.krunk.cn/emil/bib.php","bibdata":{"bibtype":"inproceedings","type":"inproceedings","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":[{"propositions":[],"lastnames":["Nokovic"],"firstnames":["Bojan"],"suffixes":[]},{"propositions":[],"lastnames":["Sekerinski"],"firstnames":["Emil"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Desai"],"firstnames":["Bipin","C."],"suffixes":[]}],"month":"August","year":"2014","pages":"3:1–3:10","bibtex":"@inproceedings{NokovicSekerinski14TimedpCharts,\n\ttitle = {Verification and {Code} {Generation} for {Timed} {Transitions} in {pCharts}},\n\tdoi = {10.1145/2641483.2641522},\n\tabstract = {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.},\n\tbooktitle = {{C3S2E} '14: {Proceedings} of the 2014 {International} {C}* {Conference} on {Computer} {Science} \\& {Software} {Engineering}},\n\tpublisher = {ACM},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\teditor = {Desai, Bipin C.},\n\tmonth = aug,\n\tyear = {2014},\n\tpages = {3:1--3:10},\n}\n\n","author_short":["Nokovic, B.","Sekerinski, E."],"editor_short":["Desai, B. C."],"key":"NokovicSekerinski14TimedpCharts","id":"NokovicSekerinski14TimedpCharts","bibbaseid":"nokovic-sekerinski-verificationandcodegenerationfortimedtransitionsinpcharts-2014","role":"author","urls":{},"metadata":{"authorlinks":{}},"downloads":1},"search_terms":["verification","code","generation","timed","transitions","pcharts","nokovic","sekerinski"],"keywords":[],"authorIDs":[],"dataSources":["fDYYrPxpzcyDvQK6b","HEdahWqKBpmSGmDwq","MF5eGzpJnqf6bSAoG","ienufKdnmJs49AsjR","So4gmSWFmbQRNEuFs","ezsmw4w22u9JFLNYJ","CvQYP6Tmpapx74Mgr","RWydLHbBJqgdeh5jr"]}