Article

RATSY – a new requirements analysis tool with synthesis

Authors:

Richard SeeberAuthors Info & Claims

CAV'10: Proceedings of the 22nd international conference on Computer Aided Verification

Pages 425 - 429

https://doi.org/10.1007/978-3-642-14295-6_37

Published: 15 July 2010 Publication History

Publisher Site

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.

References

[1]

Beazley, D.M.: SWIG: An easy to use tool for integrating scripting languages with C and C++ In: Proc 4th USENIX Tcl/Tk Workshop, pp 129-139 (1996)

Digital Library

Google Scholar

[2]

Bloem, R., Cavada, R., Pill, I., Roveri, M., Tchaltsev, A.: Rat: A tool for the formal analysis of requirements In: Damm, W., Hermanns, H (eds.) CAV 2007 LNCS, vol 4590, pp 263-267 Springer, Heidelberg (2007)

Digital Library

Google Scholar

[3]

Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV version 2: An opensource tool for symbolic model checking In: Brinksma, E., Larsen, K.G (eds.) CAV 2002 LNCS, vol 2404, pp 359-364 Springer, Heidelberg (2002)

Digital Library

Google Scholar

[4]

Dellacherie, S.: Automatic bus-protocol verification using assertions In: GSPx'04 (2004)

Google Scholar

[5]

Filiot, E., Jin, N., Raskin, J.: An antichain algorithm for LTL realizability In: Bouajjani, A., Maler, O (eds.) CAV 2009 LNCS, vol 5643, pp 263-277 Springer, Heidelberg (2009)

Digital Library

Google Scholar

[6]

Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis In: FMCAD, pp 117-124 (2006)

Digital Library

Google Scholar

[7]

Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: A tool for property synthesis In: Damm, W., Hermanns, H (eds.) CAV 2007 LNCS, vol 4590, pp 258-262 Springer, Heidelberg (2007)

Digital Library

Google Scholar

[8]

Könighofer, R., Hofferek, G., Bloem, R.: Debugging formal specifications using simple counterstrategies In: FMCAD, pp 152-159 (2009)

Google Scholar

[9]

Piterman, N., Pnueli, A., Saár, Y.: Synthesis of reactive(1) designs In: Emerson, E.A., Namjoshi, K.S (eds.) VMCAI 2006 LNCS, vol 3855, pp 364-380 Springer, Heidelberg (2005)

Digital Library

Google Scholar

[10]

Schewe, S., Finkbeiner, B.: Bounded synthesis In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y (eds.) ATVA 2007 LNCS, vol 4762, pp 474-488 Springer, Heidelberg (2007)

Digital Library

Google Scholar

[11]

Sohail, S., Somenzi, F.: Safety first: A two-stage algorithm for LTL games In: FMCAD, pp 77-84 (2009)

Google Scholar

[12]

Somenzi, F.: CUDD: CU Decision Diagram Package University of Colorado at Boulder, ftp://vlsi.colorado.edu/pub/

Google Scholar

[13]

Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae In: Emerson, E.A., Sistla, A.P (eds.) CAV 2000 LNCS, vol 1855, pp 248-263 Springer, Heidelberg (2000)

Digital Library

Google Scholar

Cited By

View all

Gorenstein AMaoz SRingert JRoychoudhury APaiva AAbreu RStorey M(2024)Kind Controllers and Fast Heuristics for Non-Well-Separated GR(1) SpecificationsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3608131(1-12)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3608131
Cappelletti LCavada RCimatti AKeppel M(2024)Towards the Formal Analysis of Algorithmic RequirementsLeveraging Applications of Formal Methods, Verification and Validation. Specification and Verification10.1007/978-3-031-75380-0_4(48-65)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-75380-0_4
Ma'ayan DMaoz SGrundy JPollock LPenta M(2023)Using Reactive Synthesis: An End-to-End Exploratory Case StudyProceedings of the 45th International Conference on Software Engineering10.1109/ICSE48619.2023.00071(742-754)Online publication date: 14-May-2023
https://dl.acm.org/doi/10.1109/ICSE48619.2023.00071
Show More Cited By

RATSY – a new requirements analysis tool with synthesis
1. Theory of computation

Recommendations

A formal requirements engineering method for specification, synthesis, and verification
SEE '97: Proceedings of the 8th International Conference on Software Engineering Environments (SEE '97)

This paper presents a formal requirements engineering method capturing specification, synthesis, and verification. Being multi-paradigm, our approach integrates individual established formal methods: temporal logics are used to express abstract ...
A source-level dynamic analysis methodology and tool for high-level synthesis
ISSS '97: Proceedings of the 10th international symposium on System synthesis

This paper presents a novel source-level dynamic analysis methodology and tool for High-Level Synthesis (HLS). It not only for the first time enables HLS to offer source-level design debugging on the `synthesized' RTL designs, but also allows the ...
An Authoring Tool for Informal and Formal Requirements Specifications
FASE '02: Proceedings of the 5th International Conference on Fundamental Approaches to Software Engineering

We describe foundations and design principles of a tool that supports authoring of informal and formal software requirements specifications simultaneously and from a single source. The tool is an attempt to bridge the gap between completely informal ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

CAV'10: Proceedings of the 22nd international conference on Computer Aided Verification

July 2010

673 pages

ISBN:364214294X

Editors:
Tayssir Touili
LIAFA, CNRS and University Paris Diderot, Paris Cedex 13, France
,
Byron Cook
LIAFA, Microsoft Research, Roger Needham Building, J J Thomson Avenue, Cambridge, UK
,
Paul Jackson
School of Informatics, University of Edinburgh, Roger Needham Building, J J Thomson Avenue, Edinburgh, UK

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 15 July 2010

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 25 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Gorenstein AMaoz SRingert JRoychoudhury APaiva AAbreu RStorey M(2024)Kind Controllers and Fast Heuristics for Non-Well-Separated GR(1) SpecificationsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3608131(1-12)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3608131
Cappelletti LCavada RCimatti AKeppel M(2024)Towards the Formal Analysis of Algorithmic RequirementsLeveraging Applications of Formal Methods, Verification and Validation. Specification and Verification10.1007/978-3-031-75380-0_4(48-65)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-75380-0_4
Ma'ayan DMaoz SGrundy JPollock LPenta M(2023)Using Reactive Synthesis: An End-to-End Exploratory Case StudyProceedings of the 45th International Conference on Software Engineering10.1109/ICSE48619.2023.00071(742-754)Online publication date: 14-May-2023
https://dl.acm.org/doi/10.1109/ICSE48619.2023.00071
Ma'ayan DMaoz SRozi RSyriani ESahraoui H(2022)Validating the correctness of reactive systems specifications through systematic explorationProceedings of the 25th International Conference on Model Driven Engineering Languages and Systems10.1145/3550355.3552425(132-142)Online publication date: 23-Oct-2022
https://dl.acm.org/doi/10.1145/3550355.3552425
Amram GMaoz SSegall IYossef MDwyer MDamian DZeller A(2022)Dynamic update for synthesized GR(1) controllersProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510054(786-797)Online publication date: 21-May-2022
https://dl.acm.org/doi/10.1145/3510003.3510054
Bensalem SCheng CHuang XKatsaros PMolin ANickovic DPeled D(2022)Formal Specification for Learning-Enabled Autonomous SystemsSoftware Verification and Formal Methods for ML-Enabled Autonomous Systems10.1007/978-3-031-21222-2_8(131-143)Online publication date: 11-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-21222-2_8
Katis AMavridou AGiannakopoulou DPressburger TSchumann J(2022)Capture, Analyze, Diagnose: Realizability Checking Of Requirements in FRETComputer Aided Verification10.1007/978-3-031-13188-2_24(490-504)Online publication date: 7-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-13188-2_24
Cavezza DAlrajeh DGyörgy A(2021)A Weakness Measure for GR(1) FormulaeFormal Aspects of Computing10.1007/s00165-020-00519-y33:1(27-63)Online publication date: 1-Jan-2021
https://dl.acm.org/doi/10.1007/s00165-020-00519-y
Mavridou AKatis AGiannakopoulou DKooi DPressburger TWhalen M(2021)From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRETFormal Methods10.1007/978-3-030-90870-6_27(503-523)Online publication date: 20-Nov-2021
https://dl.acm.org/doi/10.1007/978-3-030-90870-6_27
Maoz SShalom RDevanbu PCohen MZimmermann T(2020)Inherent vacuity for GR(1) specificationsProceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3368089.3409669(99-110)Online publication date: 8-Nov-2020
https://dl.acm.org/doi/10.1145/3368089.3409669
Show More Cited By

Abstract

References

Cited By

Recommendations

A formal requirements engineering method for specification, synthesis, and verification

A source-level dynamic analysis methodology and tool for high-level synthesis

An Authoring Tool for Informal and Formal Requirements Specifications

Comments

Information

Published In

Sponsors

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Share

Share this Publication link

Share on social media

Affiliations