Analysis and Implementation of Embedded System Models: Example of Tags in Item Management Application. Nokovic, B. & Sekerinski, E. March, 2015. ![Analysis and Implementation of Embedded System Models: Example of Tags in Item Management Application [pdf]](https://bibbase.org/img/filetypes/pdf.svg "pdf")
Paper abstract bibtex We use an application with electronic tags to illustrate a holistic development approach that includes visual modelling of the system and its environment, qualitative and quantitative verification of the model, and automated executable code generation. To this end, we use, pState, a tool for the design and verification of hierarchical state machines extended with probabilistic transitions, costs/rewards, and state invariants, called pCharts. From a pChart, pState generates input code for a probabilistic model checker in the form of either a Markov Decision Process (MDP) or a Probabilistic Timed Automaton (PTA). On the generated model, qualitative and quantitative properties can be verified. From sub-charts without probabilistic transitions, pState can generate executable code in C or assembly language. We analyze the tag collection and collision arbitration of the DASH-7 open standard protocol in which message collision is allowed to some extent. First, we create a model of tag collection to calculate collision probability and then we use the calculated collision probability to estimate the average tag power consumption. Finally, we show how the code for a tag micro-controller can be generated directly from an embedded system model.
@misc{NokovicSekerinski15TagsPresentation.pdf,
address = {Grenoble, France},
type = {Talk},
title = {Analysis and {Implementation} of {Embedded} {System} {Models}: {Example} of {Tags} in {Item} {Management} {Application}},
copyright = {https://www.date-conference.com/date15/conference/workshop-w01},
url = {https://www.cas.mcmaster.ca/~emil/pubs/NokovicSekerinski15TagsPresentation.pdf},
abstract = {We use an application with electronic tags to illustrate a holistic development approach that includes visual modelling of the system and its environment, qualitative and quantitative verification of the model, and automated executable code generation. To this end, we use, pState, a tool for the design and verification of hierarchical state machines extended with probabilistic transitions, costs/rewards, and state invariants, called pCharts. From a pChart, pState generates input code for a probabilistic model checker in the form of either a Markov Decision Process (MDP) or a Probabilistic Timed Automaton (PTA). On the generated model, qualitative and quantitative properties can be verified. From sub-charts without probabilistic transitions, pState can generate executable code in C or assembly language. We analyze the tag collection and collision arbitration of the DASH-7 open standard protocol in which message collision is allowed to some extent. First, we create a model of tag collection to calculate collision probability and then we use the calculated collision probability to estimate the average tag power consumption. Finally, we show how the code for a tag micro-controller can be generated directly from an embedded system model.},
author = {Nokovic, Bojan and Sekerinski, Emil},
month = mar,
year = {2015},
}
Downloads: 0
{"_id":"q3pz552CmiEim2yTs","bibbaseid":"nokovic-sekerinski-analysisandimplementationofembeddedsystemmodelsexampleoftagsinitemmanagementapplication-2015","authorIDs":["5d5141906acb07da0100009c","5deb78019e04d1df010000e0","5df0c9af96fa76de0100004a","5df1e05078da84de01000007","5e0152666afa18de01000079","5e14924f08c265de01000191","5e159bdce8bfcff201000064","5e1c7d5192587bde010001a6","5e1e0b00f6dca7f201000020","5e2827e2e6485dde01000035","5e288b4067e11edf01000130","5e2f394178a7cedf010000dc","5e34df5862bc74de010000f4","5e3c065bea028bde0100018f","5e4f908242a908de010000e9","5e585f852c2732de010001b4","5e5948def5822adf01000075","5e5d99be5726ecdf010000d1","5e600cdf13e3aede010001f5","5e69048f8457bade010002a1","5e6acf2ad15181f301000141","92uEQKMDcvvBMsZhM","Ge6aoqtpksMCtyrhL","YfeH5nK5eMWgp3gGy","anKewCA9AWgtndQzB","cwnpJhAGnLcWDSWqt","dochF8eFSd3jy8jcD","e6xvbhubvq5PtsszN","mixtvxbFoDFYKhAQq","oAZuP8sa3gmYvdqKk","qz4iM7vyMs82Hvx8j","wsgyLi66Pkv72928T","xset8hhxmqR8QvHh5"],"author_short":["Nokovic, B.","Sekerinski, E."],"bibdata":{"bibtype":"misc","type":"Talk","address":"Grenoble, France","title":"Analysis and Implementation of Embedded System Models: Example of Tags in Item Management Application","copyright":"https://www.date-conference.com/date15/conference/workshop-w01","url":"https://www.cas.mcmaster.ca/~emil/pubs/NokovicSekerinski15TagsPresentation.pdf","abstract":"We use an application with electronic tags to illustrate a holistic development approach that includes visual modelling of the system and its environment, qualitative and quantitative verification of the model, and automated executable code generation. To this end, we use, pState, a tool for the design and verification of hierarchical state machines extended with probabilistic transitions, costs/rewards, and state invariants, called pCharts. From a pChart, pState generates input code for a probabilistic model checker in the form of either a Markov Decision Process (MDP) or a Probabilistic Timed Automaton (PTA). On the generated model, qualitative and quantitative properties can be verified. From sub-charts without probabilistic transitions, pState can generate executable code in C or assembly language. We analyze the tag collection and collision arbitration of the DASH-7 open standard protocol in which message collision is allowed to some extent. First, we create a model of tag collection to calculate collision probability and then we use the calculated collision probability to estimate the average tag power consumption. Finally, we show how the code for a tag micro-controller can be generated directly from an embedded system model.","author":[{"propositions":[],"lastnames":["Nokovic"],"firstnames":["Bojan"],"suffixes":[]},{"propositions":[],"lastnames":["Sekerinski"],"firstnames":["Emil"],"suffixes":[]}],"month":"March","year":"2015","bibtex":"@misc{NokovicSekerinski15TagsPresentation.pdf,\n\taddress = {Grenoble, France},\n\ttype = {Talk},\n\ttitle = {Analysis and {Implementation} of {Embedded} {System} {Models}: {Example} of {Tags} in {Item} {Management} {Application}},\n\tcopyright = {https://www.date-conference.com/date15/conference/workshop-w01},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/NokovicSekerinski15TagsPresentation.pdf},\n\tabstract = {We use an application with electronic tags to illustrate a holistic development approach that includes visual modelling of the system and its environment, qualitative and quantitative verification of the model, and automated executable code generation. To this end, we use, pState, a tool for the design and verification of hierarchical state machines extended with probabilistic transitions, costs/rewards, and state invariants, called pCharts. From a pChart, pState generates input code for a probabilistic model checker in the form of either a Markov Decision Process (MDP) or a Probabilistic Timed Automaton (PTA). On the generated model, qualitative and quantitative properties can be verified. From sub-charts without probabilistic transitions, pState can generate executable code in C or assembly language. We analyze the tag collection and collision arbitration of the DASH-7 open standard protocol in which message collision is allowed to some extent. First, we create a model of tag collection to calculate collision probability and then we use the calculated collision probability to estimate the average tag power consumption. Finally, we show how the code for a tag micro-controller can be generated directly from an embedded system model.},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\tmonth = mar,\n\tyear = {2015},\n}\n\n","author_short":["Nokovic, B.","Sekerinski, E."],"key":"NokovicSekerinski15TagsPresentation.pdf","id":"NokovicSekerinski15TagsPresentation.pdf","bibbaseid":"nokovic-sekerinski-analysisandimplementationofembeddedsystemmodelsexampleoftagsinitemmanagementapplication-2015","role":"author","urls":{"Paper":"https://www.cas.mcmaster.ca/~emil/pubs/NokovicSekerinski15TagsPresentation.pdf"},"metadata":{"authorlinks":{"sekerinski, e":"https://bibbase.org/show?bib=https%3A%2F%2Fapi.krunk.cn%2Femil%2Fbib.php"}},"downloads":0},"bibtype":"misc","biburl":"https://api.krunk.cn/emil/bib.php","creationDate":"2019-08-15T00:44:32.445Z","downloads":0,"keywords":[],"search_terms":["analysis","implementation","embedded","system","models","example","tags","item","management","application","nokovic","sekerinski"],"title":"Analysis and Implementation of Embedded System Models: Example of Tags in Item Management Application","year":2015,"dataSources":["HEdahWqKBpmSGmDwq","rRazdBuE63ZLofRun","MF5eGzpJnqf6bSAoG","ienufKdnmJs49AsjR","So4gmSWFmbQRNEuFs","ezsmw4w22u9JFLNYJ","CvQYP6Tmpapx74Mgr","RWydLHbBJqgdeh5jr"]}