Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2016

Autores

Macedo, N (Autor) Outra; Brunel, J (Autor) Outra; Chemouil, D (Autor) Outra; Cunha, A (Autor) Outra; Kuperberg, D (Autor) Outra

Ata de Conferência Internacional

Título: FSE'16: PROCEEDINGS OF THE 2016 24TH ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON FOUNDATIONS OF SOFTWARE ENGINEERING

Páginas: 373-383

24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE)

Seattle, WA, NOV 13-18, 2016

Indexação

ISI Web of Knowledge - 12 Citações

Scopus - 30 Citações

Outras Informações

ID Authenticus: P-00M-7K8

DOI: 10.1145/2950290.2950318

Abstract (EN): 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.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 11