@techreport{NokovicSekerinski11PowerModelling,
	type = {{SQRL} {Report}},
	title = {Power {Modelling} and {Power} {Analysis} of {Electronic} {Tag}: {A} {Case} {Study} {Using} {Probabilistic} {Model} {Checking}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/NokovicSekerinski11PowerModelling.pdf},
	abstract = {In this work we study methods for computing the daily power consumption of an electronic tag, a battery-powered mobile device used in postal systems. First, we calculate the power consumption with “paper and pencil” by building FSM model of a device and identified all activities as possible sources of power consumption. In next step, we show how the number of activities can be reduced by combining them. Then a model is designed as a discrete-time Markov chain with rewards. Quantitative properties are specified in probabilistic linear temporal logic and automatically analyzed by the probabilistic model checker PRISM. With our model, we verify that the sleep mode accounts for the biggest share of total power consumption and that a possible decrease of power consumption during communication will not lead to a significant decrease in overall power consumption. While this calculation is done for a simple tag that is currently in use, the goal is to apply this method to more complex tags currently under development.},
	number = {63},
	institution = {McMaster University},
	author = {Nokovic, Bojan and Sekerinski, Emil},
	month = apr,
	year = {2011},
	pages = {14},
}

{"_id":"FW4ZKS6ZyF6PSB7P7","bibbaseid":"nokovic-sekerinski-powermodellingandpoweranalysisofelectronictagacasestudyusingprobabilisticmodelchecking-2011","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":"techreport","type":"SQRL Report","title":"Power Modelling and Power Analysis of Electronic Tag: A Case Study Using Probabilistic Model Checking","url":"https://www.cas.mcmaster.ca/~emil/pubs/NokovicSekerinski11PowerModelling.pdf","abstract":"In this work we study methods for computing the daily power consumption of an electronic tag, a battery-powered mobile device used in postal systems. First, we calculate the power consumption with “paper and pencil” by building FSM model of a device and identified all activities as possible sources of power consumption. In next step, we show how the number of activities can be reduced by combining them. Then a model is designed as a discrete-time Markov chain with rewards. Quantitative properties are specified in probabilistic linear temporal logic and automatically analyzed by the probabilistic model checker PRISM. With our model, we verify that the sleep mode accounts for the biggest share of total power consumption and that a possible decrease of power consumption during communication will not lead to a significant decrease in overall power consumption. While this calculation is done for a simple tag that is currently in use, the goal is to apply this method to more complex tags currently under development.","number":"63","institution":"McMaster University","author":[{"propositions":[],"lastnames":["Nokovic"],"firstnames":["Bojan"],"suffixes":[]},{"propositions":[],"lastnames":["Sekerinski"],"firstnames":["Emil"],"suffixes":[]}],"month":"April","year":"2011","pages":"14","bibtex":"@techreport{NokovicSekerinski11PowerModelling,\n\ttype = {{SQRL} {Report}},\n\ttitle = {Power {Modelling} and {Power} {Analysis} of {Electronic} {Tag}: {A} {Case} {Study} {Using} {Probabilistic} {Model} {Checking}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/NokovicSekerinski11PowerModelling.pdf},\n\tabstract = {In this work we study methods for computing the daily power consumption of an electronic tag, a battery-powered mobile device used in postal systems. First, we calculate the power consumption with “paper and pencil” by building FSM model of a device and identified all activities as possible sources of power consumption. In next step, we show how the number of activities can be reduced by combining them. Then a model is designed as a discrete-time Markov chain with rewards. Quantitative properties are specified in probabilistic linear temporal logic and automatically analyzed by the probabilistic model checker PRISM. With our model, we verify that the sleep mode accounts for the biggest share of total power consumption and that a possible decrease of power consumption during communication will not lead to a significant decrease in overall power consumption. While this calculation is done for a simple tag that is currently in use, the goal is to apply this method to more complex tags currently under development.},\n\tnumber = {63},\n\tinstitution = {McMaster University},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\tmonth = apr,\n\tyear = {2011},\n\tpages = {14},\n}\n\n","author_short":["Nokovic, B.","Sekerinski, E."],"key":"NokovicSekerinski11PowerModelling","id":"NokovicSekerinski11PowerModelling","bibbaseid":"nokovic-sekerinski-powermodellingandpoweranalysisofelectronictagacasestudyusingprobabilisticmodelchecking-2011","role":"author","urls":{"Paper":"https://www.cas.mcmaster.ca/~emil/pubs/NokovicSekerinski11PowerModelling.pdf"},"metadata":{"authorlinks":{"sekerinski, e":"https://bibbase.org/show?bib=https%3A%2F%2Fapi.krunk.cn%2Femil%2Fbib.php"}},"downloads":0},"bibtype":"techreport","biburl":"https://api.krunk.cn/emil/bib.php","creationDate":"2019-08-15T00:44:32.437Z","downloads":0,"keywords":[],"search_terms":["power","modelling","power","analysis","electronic","tag","case","study","using","probabilistic","model","checking","nokovic","sekerinski"],"title":"Power Modelling and Power Analysis of Electronic Tag: A Case Study Using Probabilistic Model Checking","year":2011,"dataSources":["HEdahWqKBpmSGmDwq","MF5eGzpJnqf6bSAoG","ienufKdnmJs49AsjR","So4gmSWFmbQRNEuFs","ezsmw4w22u9JFLNYJ","CvQYP6Tmpapx74Mgr","RWydLHbBJqgdeh5jr"]}