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 proceedingConference contributionResearchpeer-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 languageEnglish
Title of host publicationComputer Aided Verification
EditorsTayssir Toulli
PublisherSpringer
Pages425-429
Volume6174
ISBN (Print)978-3-642-14294-9
DOIs
Publication statusPublished - 2010
Event22nd International Conference on Computer Aided Verification (CAV 2010) - Edinburgh, United Kingdom
Duration: 15 Jul 201019 Jul 2010

Publication series

NameLecture Notes in Computer Science
Volume6174

Conference

Conference22nd International Conference on Computer Aided Verification (CAV 2010)
CountryUnited Kingdom
CityEdinburgh
Period15/07/1019/07/10

Fingerprint

Graphical user interfaces
Specifications
Formal specification

Fields of Expertise

  • Information, Communication & Computing

Treatment code (Nähere Zuordnung)

  • Application

Cite this

Bloem, R. P., Cimatti, A., Greimel, K., Hofferek, G., Könighofer, R., Roveri, M., ... Seeber, R. (2010). RATSY - A new Requirements Analysis Tool with Synthesis. In T. Toulli (Ed.), Computer Aided Verification (Vol. 6174, pp. 425-429). (Lecture Notes in Computer Science; Vol. 6174). Springer. https://doi.org/10.1007/978-3-642-14295-6_37

RATSY - A new Requirements Analysis Tool with Synthesis. / Bloem, Roderick Paul; Cimatti, Alessandro; Greimel, Karin; Hofferek, Georg; Könighofer, Robert; Roveri, Marco; Schuppan, Viktor; Seeber, Richard.

Computer Aided Verification. ed. / Tayssir Toulli. Vol. 6174 Springer, 2010. p. 425-429 (Lecture Notes in Computer Science; Vol. 6174).

Research output: Chapter in Book/Report/Conference proceedingConference contributionResearchpeer-review

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
Bloem RP, Cimatti A, Greimel K, Hofferek G, Könighofer R, Roveri M et al. RATSY - A new Requirements Analysis Tool with Synthesis. In Toulli T, editor, Computer Aided Verification. Vol. 6174. Springer. 2010. p. 425-429. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-14295-6_37
Bloem, Roderick Paul ; Cimatti, Alessandro ; Greimel, Karin ; Hofferek, Georg ; Könighofer, Robert ; Roveri, Marco ; Schuppan, Viktor ; Seeber, Richard. / RATSY - A new Requirements Analysis Tool with Synthesis. Computer Aided Verification. editor / Tayssir Toulli. Vol. 6174 Springer, 2010. pp. 425-429 (Lecture Notes in Computer Science).
@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",

}

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 contribution

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

ER -