A Holistic Approach in Embedded System Development

A Holistic Approach in Embedded System Development. Nokovic, B. & Sekerinski, E. In Dubois, C., Masci, P., & Méry, D., editors, Proceedings Second International Workshop on Formal Integrated Development Environment, volume 187, of Electronic Proceedings in Theoretical Computer Science, pages 72–85, June, 2015. Open Publishing Association.

Paper doi abstract bibtex

We present pState, a tool for developing “complex” embedded systems by integrating validation into the design process. The goal is to reduce validation time. To this end, qualitative and quantitative properties are specified in system models expressed as pCharts, an extended version of hierarchical state machines. These properties are specified in an intuitive way such that they can be written by engineers who are domain experts, without needing to be familiar with temporal logic. From the system model, executable code that preserves the verified properties is generated. The design is documented on the model and the documentation is passed as comments into the generated code. On the series of examples we illustrate how models and properties are specified using pState.

@inproceedings{NokovicSekerinski15HolisticEmbeddedSystem,
	series = {Electronic {Proceedings} in {Theoretical} {Computer} {Science}},
	title = {A {Holistic} {Approach} in {Embedded} {System} {Development}},
	volume = {187},
	url = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?FIDE2015.6},
	doi = {10.4204/EPTCS.187.6},
	abstract = {We present pState, a tool for developing “complex” embedded systems by integrating validation into the design process. The goal is to reduce validation time. To this end, qualitative and quantitative properties are specified in system models expressed as pCharts, an extended version of hierarchical state machines. These properties are specified in an intuitive way such that they can be written by engineers who are domain experts, without needing to be familiar with temporal logic. From the system model, executable code that preserves the verified properties is generated. The design is documented on the model and the documentation is passed as comments into the generated code. On the series of examples we illustrate how models and properties are specified using pState.},
	booktitle = {Proceedings {Second} {International} {Workshop} on {Formal} {Integrated} {Development} {Environment}},
	publisher = {Open Publishing Association},
	author = {Nokovic, Bojan and Sekerinski, Emil},
	editor = {Dubois, Catherine and Masci, Paolo and Méry, Dominique},
	month = jun,
	year = {2015},
	pages = {72--85},
}

Downloads: 0

{"_id":"uEGDTJPsTsJiWoGjj","bibbaseid":"nokovic-sekerinski-aholisticapproachinembeddedsystemdevelopment-2015","author_short":["Nokovic, B.","Sekerinski, E."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","series":"Electronic Proceedings in Theoretical Computer Science","title":"A Holistic Approach in Embedded System Development","volume":"187","url":"http://eptcs.web.cse.unsw.edu.au/paper.cgi?FIDE2015.6","doi":"10.4204/EPTCS.187.6","abstract":"We present pState, a tool for developing “complex” embedded systems by integrating validation into the design process. The goal is to reduce validation time. To this end, qualitative and quantitative properties are specified in system models expressed as pCharts, an extended version of hierarchical state machines. These properties are specified in an intuitive way such that they can be written by engineers who are domain experts, without needing to be familiar with temporal logic. From the system model, executable code that preserves the verified properties is generated. The design is documented on the model and the documentation is passed as comments into the generated code. On the series of examples we illustrate how models and properties are specified using pState.","booktitle":"Proceedings Second International Workshop on Formal Integrated Development Environment","publisher":"Open Publishing Association","author":[{"propositions":[],"lastnames":["Nokovic"],"firstnames":["Bojan"],"suffixes":[]},{"propositions":[],"lastnames":["Sekerinski"],"firstnames":["Emil"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Dubois"],"firstnames":["Catherine"],"suffixes":[]},{"propositions":[],"lastnames":["Masci"],"firstnames":["Paolo"],"suffixes":[]},{"propositions":[],"lastnames":["Méry"],"firstnames":["Dominique"],"suffixes":[]}],"month":"June","year":"2015","pages":"72–85","bibtex":"@inproceedings{NokovicSekerinski15HolisticEmbeddedSystem,\n\tseries = {Electronic {Proceedings} in {Theoretical} {Computer} {Science}},\n\ttitle = {A {Holistic} {Approach} in {Embedded} {System} {Development}},\n\tvolume = {187},\n\turl = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?FIDE2015.6},\n\tdoi = {10.4204/EPTCS.187.6},\n\tabstract = {We present pState, a tool for developing “complex” embedded systems by integrating validation into the design process. The goal is to reduce validation time. To this end, qualitative and quantitative properties are specified in system models expressed as pCharts, an extended version of hierarchical state machines. These properties are specified in an intuitive way such that they can be written by engineers who are domain experts, without needing to be familiar with temporal logic. From the system model, executable code that preserves the verified properties is generated. The design is documented on the model and the documentation is passed as comments into the generated code. On the series of examples we illustrate how models and properties are specified using pState.},\n\tbooktitle = {Proceedings {Second} {International} {Workshop} on {Formal} {Integrated} {Development} {Environment}},\n\tpublisher = {Open Publishing Association},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\teditor = {Dubois, Catherine and Masci, Paolo and Méry, Dominique},\n\tmonth = jun,\n\tyear = {2015},\n\tpages = {72--85},\n}\n\n","author_short":["Nokovic, B.","Sekerinski, E."],"editor_short":["Dubois, C.","Masci, P.","Méry, D."],"key":"NokovicSekerinski15HolisticEmbeddedSystem","id":"NokovicSekerinski15HolisticEmbeddedSystem","bibbaseid":"nokovic-sekerinski-aholisticapproachinembeddedsystemdevelopment-2015","role":"author","urls":{"Paper":"http://eptcs.web.cse.unsw.edu.au/paper.cgi?FIDE2015.6"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://api.krunk.cn/emil/bib.php","dataSources":["HEdahWqKBpmSGmDwq","MF5eGzpJnqf6bSAoG","ienufKdnmJs49AsjR","So4gmSWFmbQRNEuFs","ezsmw4w22u9JFLNYJ","CvQYP6Tmpapx74Mgr","RWydLHbBJqgdeh5jr"],"keywords":[],"search_terms":["holistic","approach","embedded","system","development","nokovic","sekerinski"],"title":"A Holistic Approach in Embedded System Development","year":2015}