Please use this identifier to cite or link to this item: http://repositorio.inesctec.pt/handle/123456789/4254
Full metadata record
DC FieldValueLanguage
dc.contributor.authorNuno Moreira Macedoen
dc.contributor.authorBrunel,Jen
dc.contributor.authorChemouil,Den
dc.contributor.authorAlcino Cunhaen
dc.contributor.authorKuperberg,Den
dc.date.accessioned2017-12-18T19:03:51Z-
dc.date.available2017-12-18T19:03:51Z-
dc.date.issued2016en
dc.identifier.urihttp://repositorio.inesctec.pt/handle/123456789/4254-
dc.identifier.urihttp://dx.doi.org/10.1145/2950290.2950318en
dc.description.abstractModel-checking is increasingly popular in the early phases of the software development process. To establish the correctness of a software design one must usually verify both structural and behavioral(or temporal) properties. Unfortunately, most specification languages, and accompanying model-checkers, excel only in analyzing either one or the other kind. This limits their ability to verify dynamic systems with rich configurations: systems whose state space is characterized by rich structural properties, but whose evolution is also expected to satisfy certain temporal properties. To address this problem, we first propose Electrum, an extension of the Alloy specification language with temporal logic operators, where both rich configurations and expressive temporal properties can easily be de fined. Two alternative model-checking techniques are then proposed, one bounded and the other unbounded, to verify systems expressed in this language, namely to verify that every desirable temporal property holds for every possible configuration.en
dc.languageengen
dc.relation5625en
dc.relation5625en
dc.relation5612en
dc.relation5612en
dc.rightsinfo:eu-repo/semantics/openAccessen
dc.titleLightweight Specification and Analysis of Dynamic Systems with Rich Configurationsen
dc.typeconferenceObjecten
dc.typePublicationen
Appears in Collections:HASLab - Articles in International Conferences

Files in This Item:
File Description SizeFormat 
P-00M-7K8.pdf631.23 kBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.