Model-based WCET Analysis with Invariants. Nokovic, B. & Sekerinski, E. In Grov, G. & Ireland, A., editors, Proceedings of the 15th International Workshop on Automated Verification of Critical Systems, AVoCS 2015, volume 72, of Electronic Communications of the EASST, pages 1–15, September, 2015. European Association of Software Science and Technology. doi abstract bibtex The integration of worst-case execution time (WCET) analysis in model-based designs allows timing problems to be discovered in the early phases of development, when they are less expensive to correct than in later phases. In this paper, we show how model-based WCET analysis can improve timing calculations com- pared to program-based WCET analysis. The models are described by hierarchical state machines with concurrency, probabilistic transition, stochastic transitions, costs/rewards attached to states and transitions, and invariants attached to states. In these models, user-specified invariants serve to check the correctness of designs by restricting allowed state configurations. Our contribution is to use invariants additionally to determine transition combinations (paths) that can be eliminated from the WCET analysis, with the help of a decision procedure, thus making the analysis more precise. The assembly code of transitions for a specific target is generated and execution time for that code calculated. From the model, a probabilistic timed automaton (PTA) or Markov decision process (MDP) can be created. On that model, execution times of transitions are calculated as costs.
@inproceedings{NokovicSekerinski15WCETinvariants,
series = {Electronic {Communications} of the {EASST}},
title = {Model-based {WCET} {Analysis} with {Invariants}},
volume = {72},
doi = {10.14279/tuj.eceasst.72.1026.1010},
abstract = {The integration of worst-case execution time (WCET) analysis in model-based designs allows timing problems to be discovered in the early phases of development, when they are less expensive to correct than in later phases. In this paper, we show how model-based WCET analysis can improve timing calculations com- pared to program-based WCET analysis. The models are described by hierarchical state machines with concurrency, probabilistic transition, stochastic transitions, costs/rewards attached to states and transitions, and invariants attached to states. In these models, user-specified invariants serve to check the correctness of designs by restricting allowed state configurations. Our contribution is to use invariants additionally to determine transition combinations (paths) that can be eliminated from the WCET analysis, with the help of a decision procedure, thus making the analysis more precise. The assembly code of transitions for a specific target is generated and execution time for that code calculated. From the model, a probabilistic timed automaton (PTA) or Markov decision process (MDP) can be created. On that model, execution times of transitions are calculated as costs.},
booktitle = {Proceedings of the 15th {International} {Workshop} on {Automated} {Verification} of {Critical} {Systems}, {AVoCS} 2015},
publisher = {European Association of Software Science and Technology},
author = {Nokovic, Bojan and Sekerinski, Emil},
editor = {Grov, Gudmund and Ireland, Andrew},
month = sep,
year = {2015},
pages = {1--15},
}
Downloads: 0
{"_id":"KntJHHddCtnnDumWZ","bibbaseid":"nokovic-sekerinski-modelbasedwcetanalysiswithinvariants-2015","author_short":["Nokovic, B.","Sekerinski, E."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","series":"Electronic Communications of the EASST","title":"Model-based WCET Analysis with Invariants","volume":"72","doi":"10.14279/tuj.eceasst.72.1026.1010","abstract":"The integration of worst-case execution time (WCET) analysis in model-based designs allows timing problems to be discovered in the early phases of development, when they are less expensive to correct than in later phases. In this paper, we show how model-based WCET analysis can improve timing calculations com- pared to program-based WCET analysis. The models are described by hierarchical state machines with concurrency, probabilistic transition, stochastic transitions, costs/rewards attached to states and transitions, and invariants attached to states. In these models, user-specified invariants serve to check the correctness of designs by restricting allowed state configurations. Our contribution is to use invariants additionally to determine transition combinations (paths) that can be eliminated from the WCET analysis, with the help of a decision procedure, thus making the analysis more precise. The assembly code of transitions for a specific target is generated and execution time for that code calculated. From the model, a probabilistic timed automaton (PTA) or Markov decision process (MDP) can be created. On that model, execution times of transitions are calculated as costs.","booktitle":"Proceedings of the 15th International Workshop on Automated Verification of Critical Systems, AVoCS 2015","publisher":"European Association of Software Science and Technology","author":[{"propositions":[],"lastnames":["Nokovic"],"firstnames":["Bojan"],"suffixes":[]},{"propositions":[],"lastnames":["Sekerinski"],"firstnames":["Emil"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Grov"],"firstnames":["Gudmund"],"suffixes":[]},{"propositions":[],"lastnames":["Ireland"],"firstnames":["Andrew"],"suffixes":[]}],"month":"September","year":"2015","pages":"1–15","bibtex":"@inproceedings{NokovicSekerinski15WCETinvariants,\n\tseries = {Electronic {Communications} of the {EASST}},\n\ttitle = {Model-based {WCET} {Analysis} with {Invariants}},\n\tvolume = {72},\n\tdoi = {10.14279/tuj.eceasst.72.1026.1010},\n\tabstract = {The integration of worst-case execution time (WCET) analysis in model-based designs allows timing problems to be discovered in the early phases of development, when they are less expensive to correct than in later phases. In this paper, we show how model-based WCET analysis can improve timing calculations com- pared to program-based WCET analysis. The models are described by hierarchical state machines with concurrency, probabilistic transition, stochastic transitions, costs/rewards attached to states and transitions, and invariants attached to states. In these models, user-specified invariants serve to check the correctness of designs by restricting allowed state configurations. Our contribution is to use invariants additionally to determine transition combinations (paths) that can be eliminated from the WCET analysis, with the help of a decision procedure, thus making the analysis more precise. The assembly code of transitions for a specific target is generated and execution time for that code calculated. From the model, a probabilistic timed automaton (PTA) or Markov decision process (MDP) can be created. On that model, execution times of transitions are calculated as costs.},\n\tbooktitle = {Proceedings of the 15th {International} {Workshop} on {Automated} {Verification} of {Critical} {Systems}, {AVoCS} 2015},\n\tpublisher = {European Association of Software Science and Technology},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\teditor = {Grov, Gudmund and Ireland, Andrew},\n\tmonth = sep,\n\tyear = {2015},\n\tpages = {1--15},\n}\n\n","author_short":["Nokovic, B.","Sekerinski, E."],"editor_short":["Grov, G.","Ireland, A."],"key":"NokovicSekerinski15WCETinvariants","id":"NokovicSekerinski15WCETinvariants","bibbaseid":"nokovic-sekerinski-modelbasedwcetanalysiswithinvariants-2015","role":"author","urls":{},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://api.krunk.cn/emil/bib.php","dataSources":["HEdahWqKBpmSGmDwq","MF5eGzpJnqf6bSAoG","ienufKdnmJs49AsjR","So4gmSWFmbQRNEuFs","ezsmw4w22u9JFLNYJ","CvQYP6Tmpapx74Mgr","RWydLHbBJqgdeh5jr"],"keywords":[],"search_terms":["model","based","wcet","analysis","invariants","nokovic","sekerinski"],"title":"Model-based WCET Analysis with Invariants","year":2015}