Concrete artefacts are produced and used for dissemination. These include scientific publications, a repository of use-cases, tutorials, a non-technical article presenting the main achievements of the project, material for tutorials and recorded tutorials. These artefacts will remain available to the general public beyond the duration of the project and promote a continuative and long-term dissemination.

If you are unable to view these files, please log in or register.

Description: Conversion from/to Mungo usages to a suitable form of finite state automata with internal and external non-determinism Developed at: NOVA Contacts: aravara@fct.unl.pt, jd.mota@campus.fct.unl.pt Available at: https://jdmota.github.io/mungo-typestate-parser/

Description: TRAC is a tool for the specification and verification of coordinated multiparty distributed systems. Relying on finite-state machines (FSMs) where transition labels look like Hoare triples, TRAC can specify the

T2

Description: Automatic program verification tool for proving temporal properties of programs, such as safety, termination, or properties specified in the logic CTL. T2 can work directly on C programs. Developed at:

Description: Test driver of RESTful API based on binary session types. The tool features a domain-specific language for OpenAPI specifications, COpenAPI, that enables the modelling of communication protocols between a

Description: SEArch, after Service Execution Architecture, is a language-independent execution infrastructure capable of performing transparent dynamic reconfiguration of software artefacts. SEArch exploits Choreographic mechanisms to specify interoperability contracts, thus providing the

Description: Allows the user to define global views in terms of global choreographies, (2) verifies realisability of the global view and identifies all possible misbehaviors that could arise from a message-passing

Description: The tool implements a well founded notion of protocol composition (which preserves progress, fairness and honours user-defined constraints expressed as assertions), and also allows to generate Erlang code (stubs) from

Description: The adoption of formal models by process specialists has faced two challenges: First, it requires process specialists to get training in formal modeling. Second, the resulting specifications bear little resemblance