RATSY - A New Requirements Analysis Tool with Synthesis

Formal specifications play an increasingly important role in system design-flows. 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 B¨uchi word automata. Second, it can help debug incorrect specifications 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.

• Type: Conference
• Year: 2010
• Where: CAV
• Authors: Roderick Bloem, Alessandro Cimatti, Karin Greimel, Georg Hofferek, Robert Könighofer, Marco Roveri, Viktor Schuppan, Richard Seeber
• Keywords: Analysis Tool RAT, CAV 2010, Debug Incorrect Specifications, Hardware, Ratsy Extends Rat