Verifying Statecharts with State Invariants. Sekerinski, E. In Breitman, K., Woodcock, J., Sterritt, R., & Hinchey, M., editors, 13th IEEE International Conference on Engineering of Complex Computer Systems, of ICECCS '08, pages 7–14, Belfast, Northern Ireland, March, 2008. IEEE Computer Society. doi abstract bibtex 1 download Statecharts are an executable visual language for specifying the reactive behavior of systems. We propose to statically verify the design expressed by a statechart by allowing individual states to be annotated with invariants and checking the consistency of the invariants with the transitions. We present an algorithm that uses the locality of state invariants for generating “many small” verification conditions that should be more amenable to automatic checking than an approach based on a single global invariant.
@inproceedings{Sekerinski08StateInvariants,
address = {Belfast, Northern Ireland},
series = {{ICECCS} '08},
title = {Verifying {Statecharts} with {State} {Invariants}},
doi = {http://dx.doi.org/10.1109/ICECCS.2008.40},
abstract = {Statecharts are an executable visual language for specifying the reactive behavior of systems. We propose to statically verify the design expressed by a statechart by allowing individual states to be annotated with invariants and checking the consistency of the invariants with the transitions. We present an algorithm that uses the locality of state invariants for generating “many small” verification conditions that should be more amenable to automatic checking than an approach based on a single global invariant.},
booktitle = {13th {IEEE} {International} {Conference} on {Engineering} of {Complex} {Computer} {Systems}},
publisher = {IEEE Computer Society},
author = {Sekerinski, Emil},
editor = {Breitman, K. and Woodcock, J. and Sterritt, R. and Hinchey, M.},
month = mar,
year = {2008},
pages = {7--14},
}
Downloads: 1
{"_id":"FjZ3yP4ubSqP3hDM6","bibbaseid":"sekerinski-verifyingstatechartswithstateinvariants-2008","downloads":1,"creationDate":"2019-02-02T15:48:53.590Z","title":"Verifying Statecharts with State Invariants","author_short":["Sekerinski, E."],"year":2008,"bibtype":"inproceedings","biburl":"https://api.krunk.cn/emil/bib.php","bibdata":{"bibtype":"inproceedings","type":"inproceedings","address":"Belfast, Northern Ireland","series":"ICECCS '08","title":"Verifying Statecharts with State Invariants","doi":"http://dx.doi.org/10.1109/ICECCS.2008.40","abstract":"Statecharts are an executable visual language for specifying the reactive behavior of systems. We propose to statically verify the design expressed by a statechart by allowing individual states to be annotated with invariants and checking the consistency of the invariants with the transitions. We present an algorithm that uses the locality of state invariants for generating “many small” verification conditions that should be more amenable to automatic checking than an approach based on a single global invariant.","booktitle":"13th IEEE International Conference on Engineering of Complex Computer Systems","publisher":"IEEE Computer Society","author":[{"propositions":[],"lastnames":["Sekerinski"],"firstnames":["Emil"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Breitman"],"firstnames":["K."],"suffixes":[]},{"propositions":[],"lastnames":["Woodcock"],"firstnames":["J."],"suffixes":[]},{"propositions":[],"lastnames":["Sterritt"],"firstnames":["R."],"suffixes":[]},{"propositions":[],"lastnames":["Hinchey"],"firstnames":["M."],"suffixes":[]}],"month":"March","year":"2008","pages":"7–14","bibtex":"@inproceedings{Sekerinski08StateInvariants,\n\taddress = {Belfast, Northern Ireland},\n\tseries = {{ICECCS} '08},\n\ttitle = {Verifying {Statecharts} with {State} {Invariants}},\n\tdoi = {http://dx.doi.org/10.1109/ICECCS.2008.40},\n\tabstract = {Statecharts are an executable visual language for specifying the reactive behavior of systems. We propose to statically verify the design expressed by a statechart by allowing individual states to be annotated with invariants and checking the consistency of the invariants with the transitions. We present an algorithm that uses the locality of state invariants for generating “many small” verification conditions that should be more amenable to automatic checking than an approach based on a single global invariant.},\n\tbooktitle = {13th {IEEE} {International} {Conference} on {Engineering} of {Complex} {Computer} {Systems}},\n\tpublisher = {IEEE Computer Society},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Breitman, K. and Woodcock, J. and Sterritt, R. and Hinchey, M.},\n\tmonth = mar,\n\tyear = {2008},\n\tpages = {7--14},\n}\n\n","author_short":["Sekerinski, E."],"editor_short":["Breitman, K.","Woodcock, J.","Sterritt, R.","Hinchey, M."],"key":"Sekerinski08StateInvariants","id":"Sekerinski08StateInvariants","bibbaseid":"sekerinski-verifyingstatechartswithstateinvariants-2008","role":"author","urls":{},"metadata":{"authorlinks":{}},"downloads":1},"search_terms":["verifying","statecharts","state","invariants","sekerinski"],"keywords":[],"authorIDs":[],"dataSources":["fDYYrPxpzcyDvQK6b","HEdahWqKBpmSGmDwq","MF5eGzpJnqf6bSAoG","RfxodDQazHHccThPz","ienufKdnmJs49AsjR","So4gmSWFmbQRNEuFs","ezsmw4w22u9JFLNYJ","CvQYP6Tmpapx74Mgr","RWydLHbBJqgdeh5jr"]}