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
Volume	6174
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.pdfFinal published version, 249 KB

EU - DIAMOND - Diagnosis, Error Modelling and Correction for Reliable Systems Design
Khalimov, A., Greimel, K., Jacobs, S., Hofferek, G., Könighofer, B., Könighofer, R. & Bloem, R.
1/01/10 → 31/12/12
Project: Research project
Formal Methods for Design & Verification
Jacobs, S., Bloem, R., Könighofer, R., Könighofer, B., Khalimov, A., Hofferek, G. & Braud-Santoni, N.
1/02/08 → 15/07/19
Project: Research area
EU - COCONUT - A correct-by-construction workbench for design and verification of embedded systems
Könighofer, R., Hofferek, G., Greimel, K. & Bloem, R.
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. vol. 6174, 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 insystem design-flows. Yet, they are not always easy to deal with. In thispaper we present RATSY, a successor of the Requirements AnalysisTool RAT. RATSY extends RAT in several ways. First, it includes anew graphical user interface to specify system properties as simple B{\"u}chiword automata. Second, it can help debug incorrect specifications bymeans of a game-based approach. Third, it allows correct-by-constructionsynthesis of systems from their temporal properties. These new featuresand 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",

volume = "6174",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "425--429",

editor = "Tayssir Toulli",

booktitle = "Computer Aided Verification",

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 insystem design-flows. Yet, they are not always easy to deal with. In thispaper we present RATSY, a successor of the Requirements AnalysisTool RAT. RATSY extends RAT in several ways. First, it includes anew graphical user interface to specify system properties as simple Büchiword automata. Second, it can help debug incorrect specifications bymeans of a game-based approach. Third, it allows correct-by-constructionsynthesis of systems from their temporal properties. These new featuresand their seamless integration assist in property-based design processes.

AB - Formal specifications play an increasingly important role insystem design-flows. Yet, they are not always easy to deal with. In thispaper we present RATSY, a successor of the Requirements AnalysisTool RAT. RATSY extends RAT in several ways. First, it includes anew graphical user interface to specify system properties as simple Büchiword automata. Second, it can help debug incorrect specifications bymeans of a game-based approach. Third, it allows correct-by-constructionsynthesis of systems from their temporal properties. These new featuresand 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

VL - 6174

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

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