Skip to content

Latest commit

 

History

History
34 lines (23 loc) · 2.14 KB

readme.md

File metadata and controls

34 lines (23 loc) · 2.14 KB
Raw

Featured Extended Team Automata (FETA)

FETA is a formalism to reason about communication safety in families (or software product lines) of teams, which are systems of reactive components that communicate according to specified synchronisation types.

This repository provides a prototype tool to specify and analysis FETA. Currently, it is possible to try the tool online at

To compile and run locally these analysis using a web frontend you need to compile and run the code from a specific branch of the ReoLive repository, available at https://github.com/ReoLanguage/ReoLive/tree/feta-only.

When running the tool you will be able to:

  • specify Extended Team Automata (ETA) and Feature Extended Team Automata (FETA);
  • Infer how many products of the Featured family exist, how many states, how many transitions, and other properties;
  • Visualise the global automaton, both before and after applying the synchronisation policies;
  • Visualise the automata of the individual components;
  • Generate logical formulas that characterise receptiveness and responsiveness, and their weak counterparts of a single ETA;
  • Use mCRL2 model checker to infer whether the ETA is receptive and responsive, producing counter-examples when not.

Publications

  • (2021) Featured Team Automata. Maurice H. ter Beek, Guillermina Cledou, Rolf Hennicker, José Proença. Formal Methods - 24th international symposium, FM 2019, Beijing, China, November 20-26, 2021, LNCS 13047.

  • (2023) Can we Communicate? Using Dynamic Logic to Verify Team Automata. Maurice H. ter Beek, Guillermina Cledou, Rolf Hennicker, José Proença. Formal Methods - 26th international symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, LNCS 14000.

Developers