Formal specications play an increasingly important role in system design- ows. Yet, they are not always easy to deal with. In this paper we present RATSY, a successor of the Requirements Analysis Tool RAT. RATSY extends RAT in several ways. First, it includes a new graphical user interface to specify system properties as simple Buchi word automata. Second, it can help debug incorrect specications by means of a game-based approach. Third, it allows correct-by-construction synthesis of systems from their temporal properties. These new features and their seamless integration assist in property-based design processes.
RATSY - A new Requirements Analysis Tool with Synthesis / Bloem, Roderick; Cimatti, Alessandro; Greimel, Karin; Hofferek, Georg; Koenighofer, Robert; Roveri, Marco; Schuppan, Viktor; Seeber, Richard. - 6174:(2010), pp. 425-429. (Intervento presentato al convegno CAV 2010 tenutosi a Edinburgh, UK nel 15-19/07/2010).
RATSY - A new Requirements Analysis Tool with Synthesis
Alessandro Cimatti;Marco Roveri;
2010-01-01
Abstract
Formal specications play an increasingly important role in system design- ows. Yet, they are not always easy to deal with. In this paper we present RATSY, a successor of the Requirements Analysis Tool RAT. RATSY extends RAT in several ways. First, it includes a new graphical user interface to specify system properties as simple Buchi word automata. Second, it can help debug incorrect specications by means of a game-based approach. Third, it allows correct-by-construction synthesis of systems from their temporal properties. These new features and their seamless integration assist in property-based design processes.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione