I tool utilizzati nell’ambito del progetto PROSSIMO, attualmente, sono quelli contenuti all’interno della SAGE Verification Suite sviluppata dal Laboratorio SAGE, nato dalla collaborazione tra il laboratorio IDEA dell’Università di Sassari ed il laboratorio AIMS dell’Università di Genova. Tale suite rappresenta una collezione di strumenti software che si occupa, a diversi livelli, di verifica e modellazione di sistemi complessi quali i Cyber-Physical Systems (CPSs).

 

 

ReqV is a tool for formal consistency checking of requirements. The main goal of the tool is to provide an easy-to-use environment for the verification of requirements in Cyber-Physical Systems (CPSs). Reqv takes as input a set of requirements expressed in a structured natural language, translates them in a formal language and it checks their inner consistency. In case of failure, ReqV can also extracts a minimal set of conflicting requirements to help designers in correcting the specification.

ReqV is freely available under GPL license at https://gitlab.sagelab.it/sage/ReqV.

More info: http://www.sagelab.it/reqv/.


Hydra is a domain-independent tool for Goal-Oriented control of Cyber-Physical Systems. Using state of the art techniques in AI Planning, Satisfiability Modulo Theories and Numeric Optimization, Hydra lets you derive goal-oriented, correct by construction strategies from high-level model of Hybrid Systems.

Hydra is freely available under the LGPL license at https://gitlab.sagelab.it/sage/hydra.

More info: http://www.sagelab.it/hydra/.