RATSY - A new Requirements Analysis Tool with Synthesis

Roderick Paul Bloem; Alessandro Cimatti; Karin Greimel; Georg Hofferek; Robert Könighofer; Marco Roveri; Viktor Schuppan; Richard Seeber

doi:10.1007/978-3-642-14295-6_37

RATSY - A new Requirements Analysis Tool with Synthesis

Roderick Paul Bloem
, Alessandro Cimatti
, Karin Greimel
, Georg Hofferek
, Robert Könighofer
, Marco Roveri
, Viktor Schuppan
, Richard Seeber

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

Abstract

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üchi 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.

Original language	English
Title of host publication	Computer Aided Verification
Editors	Tayssir Toulli
Publisher	Springer
Pages	425-429
ISBN (Print)	978-3-642-14294-9
DOIs	https://doi.org/10.1007/978-3-642-14295-6_37
Publication status	Published - 2010
Event	22nd International Conference on Computer Aided Verification (CAV 2010) - Edinburgh, United Kingdom Duration: 15 Jul 2010 → 19 Jul 2010

Publication series

Name	Lecture Notes in Computer Science
Volume	6174

Conference

Conference	22nd International Conference on Computer Aided Verification (CAV 2010)
Country/Territory	United Kingdom
City	Edinburgh
Period	15/07/10 → 19/07/10

Fields of Expertise

Information, Communication & Computing

Treatment code (Nähere Zuordnung)

Application

Access to Document

10.1007/978-3-642-14295-6_37

paper_as_submitted_to_CAV.pdfAccepted author manuscript, 249 KB

EU - DIAMOND - Diagnosis, Error Modelling and Correction for Reliable Systems Design
Könighofer, R. (Attendee / Assistant), Jacobs, S. (Attendee / Assistant), Greimel, K. (Attendee / Assistant), Hofferek, G. (Contact person), Bloem, R. (Project manager), Khalimov, A. (Attendee / Assistant) & Könighofer, B. (Attendee / Assistant)
1/01/10 → 31/12/12
Project: Research project
Formal Methods for Design & Verification
Könighofer, R. (Attendee), Hofferek, G. (Attendee), Jacobs, S. (Attendee), Bloem, R. (Coordinator), Braud-Santoni, N. (Attendee), Khalimov, A. (Attendee) & Könighofer, B. (Attendee)
1/02/08 → 15/07/19
Project: Research area
EU - COCONUT - A correct-by-construction workbench for design and verification of embedded systems
Greimel, K. (Attendee / Assistant), Hofferek, G. (Attendee / Assistant), Bloem, R. (Project manager) & Könighofer, R. (Attendee / Assistant)
1/01/08 → 30/06/10
Project: Research project

Cite this

Bloem, RP, Cimatti, A, Greimel, K, Hofferek, G, Könighofer, R, Roveri, M, Schuppan, V & Seeber, R 2010, RATSY - A new Requirements Analysis Tool with Synthesis. in T Toulli (ed.), Computer Aided Verification. Lecture Notes in Computer Science, vol. 6174, Springer, pp. 425-429, 22nd International Conference on Computer Aided Verification (CAV 2010), Edinburgh, United Kingdom, 15/07/10. https://doi.org/10.1007/978-3-642-14295-6_37

@inproceedings{e0e058d3d928439fad748155e7b0b3d1,

title = "RATSY - A new Requirements Analysis Tool with Synthesis",

abstract = "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{\"u}chi 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.",

author = "Bloem, \{Roderick Paul\} and Alessandro Cimatti and Karin Greimel and Georg Hofferek and Robert K{\"o}nighofer and Marco Roveri and Viktor Schuppan and Richard Seeber",

year = "2010",

doi = "10.1007/978-3-642-14295-6\_37",

language = "English",

isbn = "978-3-642-14294-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "425--429",

editor = "Tayssir Toulli",

booktitle = "Computer Aided Verification",

address = "United States",

note = "22nd International Conference on Computer Aided Verification (CAV 2010) ; Conference date: 15-07-2010 Through 19-07-2010",

}

TY - GEN

T1 - RATSY - A new Requirements Analysis Tool with Synthesis

AU - Bloem, Roderick Paul

AU - Cimatti, Alessandro

AU - Greimel, Karin

AU - Hofferek, Georg

AU - Könighofer, Robert

AU - Roveri, Marco

AU - Schuppan, Viktor

AU - Seeber, Richard

PY - 2010

Y1 - 2010

N2 - 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üchi 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.

AB - 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üchi 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.

U2 - 10.1007/978-3-642-14295-6_37

DO - 10.1007/978-3-642-14295-6_37

M3 - Conference paper

SN - 978-3-642-14294-9

T3 - Lecture Notes in Computer Science

SP - 425

EP - 429

BT - Computer Aided Verification

A2 - Toulli, Tayssir

PB - Springer

T2 - 22nd International Conference on Computer Aided Verification (CAV 2010)

Y2 - 15 July 2010 through 19 July 2010

ER -

RATSY - A new Requirements Analysis Tool with Synthesis

Abstract

Publication series

Conference

Fields of Expertise

Treatment code (Nähere Zuordnung)

Access to Document

Fingerprint

Projects

EU - DIAMOND - Diagnosis, Error Modelling and Correction for Reliable Systems Design

Formal Methods for Design & Verification

EU - COCONUT - A correct-by-construction workbench for design and verification of embedded systems

Cite this