The main goal of this project is to develop a methodology for trustworthy software design that is both formal, unified, and lightweight. By "formal" we mean a methodology that is based on a specification language with a precise semantics and supported by rigorous V&V techniques. By "unified" we mean a methodology that covers many key aspects of software design with a single unifying formalism and an integrated toolset. And by "lightweight" we mean a methodology that is (a) easy to grasp by software engineers, allowing them to quickly capture the essence of the system under design, (b) flexible to adapt to their prefered styles of specification and (c) supported by automated V&V, the all-important ingredient in any trustworthy design. In short, we want to develop a methodology that has some of the key features that industry seeks when choosing a design language and methodology: be able to "handle very large, complex or subtle problems", "minimize cognitive burden", and have "high return on investment".
Many design methodologies and languages have been proposed in the past, but we believe none of them achieved the right blend of the three characteristics stressed above. Either they are too informal, or they focus on a very specific aspect of design, or they are not lightweight, namely not supported by automated V&V tools. A particular formal specification language that excels in two of these characteristics, namely, being both formal and lightweight, is Alloy. Alloy is a formal modeling language based on relational logic, a variant of first-order logic where predicates can be combined using relational operators, further extended with transitive closure to allow the specification of reachability properties. This so-called relational logic is quite easy to grasp, and allows a very simple specification style, quite often resembling natural language. Alloy is also supported by an Analyzer that enables model validation and automatic (bounded) verification by translation to off-the-shelf SAT solvers. The tool finds examples and counterexamples that are depicted visually, greatly simplifying the design validation process. Due to this powerful combination of formality and lightweightness, Alloy has become increasingly popular in recent years.
Unfortunately, while great for conceptual design, namely to specify and reason about structural properties, Alloy still has some shortcomings that difficult its application to other aspects of software design. Thus, to achieve the above stated goal, we plan to extend Alloy and its Analyzer with several new features, such as, temporal logic to allow the specification of dynamic properties, support for variability modeling, support for the specification and verification of software architectures, a more efficient verification engine, or better support for scenario exploration.
- Alcino Cunha, PhD, HASLab (Principal Investigator)
- Alexandre Madeira, PhD, HASLab
- Chong Liu, MSc, HASLab
- Bruno Cancelinha, BSc, HASLab
- David Chemouil, PhD, ONERA
- Eduardo Pessoa, BSc, HASLab
- José Creissac Campos, PhD, HASLab
- José Nuno Macedo, BSc, HASLab
- José Pereira, BSc, HASLab
- José Proença, PhD, HASLab
- José Nuno Oliveira, PhD, HASLab
- Julien Brunel, PhD, ONERA
- Leandro Gomes, MSc, HASLab
- Luis Soares Barbosa, PhD, HASLab
- Maria Guillermina Cledou, MSc, HASLab
- Michael Harrison, PhD, Newcastle University
- Nuno Macedo, PhD, HASLab
- Paolo Masci, PhD, HASLab
- Renato Carvalho, BSc, HASLab
- Renato Neves, MSc, HASLab
- Rui Couto, PhD, HASLab
- José Proença and Dave Clarke: Typed connector families and their semantics. Science of Computer Programming, volume 146, pages 28-49. Elsevier, 2017.
- José N. Oliveira: Programming from Metaphorisms. Journal of Logical and Algebraic Methods in Programming, volume 94, pages 15-44. Elsevier, 2018.
- Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha, and Denis Kuperberg: Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations. In proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 373-383. ACM, 2016.
- Denis Kuperberg, Julien Brunel, and David Chemouil: On Finite Domains in First-Order Linear Temporal Logic. In proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, volume 9938 of LNCS, pages 211-226. Springer, 2016.
- Guillermina Cledou, José Proença, and Luis Barbosa: Composing families of Timed Automata. In proceedings of the 7th International Conference on Fundamentals of Software Engineering, volume 10522 of LNCS, pages 51-66. Springer, 2017.
- Nuno Macedo, Alcino Cunha, and Eduardo Pessoa: Exploiting Partial Knowledge for Efficient Model Analysis. In proceedings of the 15th International Symposium on Automated Technology for Verification and Analysis, volume 10482 of LNCS, pages 344-362. Springer, 2017.
- Miguel Pinto, Marcelo Gonçalves, Paolo Masci and José Creissac Campos: TOM: a Model-Based GUI Testing framework. In proceedings of the 14th International Conference on Formal Aspects of Component Software, volume 10487 of LNCS, pages 155-161. Springer, 2017.
- Guillermina Cledou, José Proença, and Luis Barbosa: An Refinement Relation for Families of Timed Automata. In proceedings of the 20th Brazilian Symposium on Formal Methods, volume 10623 of LNCS, pages 161-178. Springer, 2017.
- Alcino Cunha and Nuno Macedo: Validating the Hybrid ERTMS/ETCS Level 3 Concept with Electrum. In proceedings of the 6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, volume 10817 of LNCS, pages 307-321. Springer, 2018
- Julien Brunel, David Chemouil, Alcino Cunha, Thomas Hujsa, Nuno Macedo, and Jeanne Tawa: Proposition of an Action Layer for Electrum. In proceedings of the 6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, volume 10817 of LNCS, pages 397-402. Springer, 2018.
- Rui Couto, José Creissac Campos, Nuno Macedo, and Alcino Cunha: Improving the Visualization of Alloy Instances. In proceedings of the 4th International Workshop on Formal Integrated Development Environment. 2018.
- Julien Brunel, David Chemouil, Alcino Cunha, and Nuno Macedo: The Electrum Analyzer: Model Checking Relational First-Order Temporal Specifications. In proceedings of the 33rd IEEE/ACM International Conference on Automated Software Engineering, pages 884-887. ACM, 2018.
- Julien Brunel, David Chemouil, and Jeanne Tawa: Analyzing the Fundamental Liveness Property of the Chord Protocol. In proceedings of the 18th International Conference on Formal Methods in Computer-Aided Design. 2018. To appear.
- Chong Liu: Lightweight Trustworthy High-level Software Design. PhD thesis. Ongoing.
- Guillermina Cledou: A Virtual Factory for Smart City Service Integration. PhD thesis. Ongoing.
- Bruno Cancelinha: Model checking Electrum specifications. MSc thesis. Ongoing.
- Eduardo Pessoa: Parallel verification of Dynamics Systems with Rich Configurations. MSc thesis. December, 2016.
- José Pereira: A Web-based social environment for Alloy. MSc thesis. December, 2016.
- Renato Carvalho: Analysis of message passing software using Electrum. MSc thesis. Ongoing.