Abstract

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.

Team

Workshops

Books

  1. Julien Brunel, David Chemouil, Alcino Cunha, and Nuno Macedo: Formal Software Design. 2020. In progress.

Journal articles

  1. José Proença and Dave Clarke: Typed connector families and their semantics. Science of Computer Programming, volume 146, pages 28-49. Elsevier, 2017.
  2. José N. Oliveira: Programming from Metaphorisms. Journal of Logical and Algebraic Methods in Programming, volume 94, pages 15-44. Elsevier, 2018.
  3. Alcino Cunha and Nuno Macedo: Validating the Hybrid ERTMS/ETCS Level 3 Concept with Electrum. International Journal on Software Tools for Technology Transfer, volume 22, number 3, pages 281-296. Springer, 2020.
  4. J.C. Campos, C. Fayollas, M.D. Harrison, C. Martinie, P. Masci, and P. Palanque: Supporting the analysis of safety critical user interfaces: an exploration of three formal tools. ACM Transactions on Computer-Human Interaction, volume 27, issue 5, article 35, pages 1-48. ACM, 2020.
  5. Quentin Peyras, Julien Brunel, David Chemouil: A Decidable and Expressive Fragment of Many-Sorted First-Order Linear Temporal Logic. Information and Computation. Elsevier. To appear.
  6. Julien Brunel, David Chemouil, Alcino Cunha, and Nuno Macedo: Pardinus: A temporal relational model finder. Under submission.

Conference papers

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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, pages 1-9. IEEE, 2018.
  12. Rui Couto and José Creissac Campos: Improving Traces Visualisation through Layout Managers. In proceedings of the 1st International Conference on Graphics and Interaction, pages 1-8. IEEE, 2018.
  13. Jean-Paul Bodeveix, Julien Brunel, David Chemouil and Mamoun Filali-Amine: Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol. In proceedings of the 23rd International Symposium on Formal Methods, volume 11800 of LNCS, pages 45-63. Springer, 2019.
  14. Chong Liu, Nuno Macedo, and Alcino Cunha: Simplifying the analysis of software design variants with a colorful Alloy. In proceedings of the 3rd International Symposium on Dependable Software Engineering, volume 11951 of LNCS, pages 38-55. Springer, 2019.
  15. Julien Brunel, David Chemouil, Alcino Cunha, and Nuno Macedo: Simulation under arbitrary temporal logic constraints. In proceedings of the 5th International Workshop on Formal Integrated Development Environment, volume 310 of EPTCS, pages 63-69. 2019.
  16. Quentin Peyras, Julien Brunel, and David Chemouil: A Bounded Domain Property for an Expressive Fragment of First-Order Linear Temporal Logic. In proceedings of the 26th International Symposium on Temporal Representation and Reasoning, pages 15:1-15:16. 2019.
  17. Leandro Gomes, Alexandre Madeira, and Mario R. F. Benevides: Logics for Petri Nets with Propagating Failures. In proceedings of the 8th International Conference on Fundamentals of Software Engineering, volume 11761 of LNCS, pages 145-157. Springer, 2019.
  18. Alcino Cunha, Nuno Macedo, and Chong Liu: Validating Multiple Variants of an Automotive Light System with Electrum. In proceedings of the 7th International Conference on Rigorous State Based Methods, volume 12071 of LNCS, pages 318-334. Springer, 2020.
  19. Nuno Macedo, Alcino Cunha, José Pereira, Renato Carvalho, Ricardo Silva, Ana C. R. Paiva, Miguel Sozinho Ramalho, and Daniel Silva: Experiences on Teaching Alloy with an Automated Assessment Platform. In proceedings of the 7th International Conference on Rigorous State Based Methods, volume 12071 of LNCS, pages 61-77. Springer, 2020.
  20. Renato Carvalho, Alcino Cunha, Nuno Macedo, and André Santos: Verification of system-wide safety properties of ROS applications. In proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems. IEEE, 2020. To appear.

Other publications

  1. Nuno Macedo, Alcino Cunha, José Pereira, Renato Carvalho, Ricardo Silva, Ana C. R. Paiva, Miguel S. Ramalho, Daniel Castro Silva: Sharing and Learning Alloy on the Web. CoRR abs/1907.02275, 2019.

Thesis

  1. Chong Liu: Lightweight Trustworthy High-level Software Design. PhD thesis. January, 2022.
  2. Guillermina Cledou: A Virtual Factory for Smart City Service Integration. PhD thesis. November, 2018.
  3. Bruno Cancelinha: Model checking Electrum specifications. MSc thesis. December, 2019.
  4. Eduardo Pessoa: Parallel verification of Dynamics Systems with Rich Configurations. MSc thesis. December, 2016.
  5. José Pereira: A Web-based social environment for Alloy. MSc thesis. December, 2016.
  6. Renato Carvalho: Analysis of message passing software using Electrum. MSc thesis. November, 2020.

Tools