Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations

dc.contributor.author Nuno Moreira Macedo en
dc.contributor.author Brunel,J en
dc.contributor.author Chemouil,D en
dc.contributor.author Alcino Cunha en
dc.contributor.author Kuperberg,D en
dc.date.accessioned 2017-12-18T19:03:51Z
dc.date.available 2017-12-18T19:03:51Z
dc.date.issued 2016 en
dc.description.abstract Model-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.identifier.uri http://repositorio.inesctec.pt/handle/123456789/4254
dc.identifier.uri http://dx.doi.org/10.1145/2950290.2950318 en
dc.language eng en
dc.relation 5625 en
dc.relation 5625 en
dc.relation 5612 en
dc.relation 5612 en
dc.rights info:eu-repo/semantics/openAccess en
dc.title Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations en
dc.type conferenceObject en
dc.type Publication en
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
P-00M-7K8.pdf
Size:
631.23 KB
Format:
Adobe Portable Document Format
Description: