Abstract
Formal languages are increasingly used to describe the functional requirements of circuits. Although formal requirements can be hard to understand and subtle, they are seldom the object of verification. In this paper we present our requirement analysis tool, RAT. Our tool supports quality assurance of formal specifications. A designer can interactively explore the requirements’ semantics and automatically check the specification against assertions (which must be satisfied) and possibilities (which describe allowed corner-case behavior). Using RAT, a designer can also investigate the realizability of a specification. RAT was successfully examined in several industrial projects.
Supported by the European Commission under contract 507219 (PROSYD).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Accellera. Property specification language — reference manual, version 1.01 (April 2003)
Auerbach, G., Benalycherif, L., Fedeli, A., Fisman, D., McIsaac, A., Winkelmann, K.: Case studies in property-based requirements specification, Prosyd Delivarable D1.4/1 (November 2006), http://www.prosyd.org
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Bloem, R., Cavada, R., Eisner, C., Pill, I., Roveri, M., Semprini, S.: Manual for property simulation and property assurance tool, Prosyd Delivarable D1.2/4-5 (November 2005), http://www.prosyd.org
Bloem, R., Galler, S., Jobstman, B., Weiglhofer, M., Piterman, N., Pnueli, A.: Automatic hardware synthesis from specifications: A case study. In: Proceeding of DATE 2007 (to appear, 2007)
Brayton, R.K., et al.: A system for verification and synthesis. In: Henzinger, T., Alur, R. (eds.) CAV 1996. LNCS, vol. 1102, pp. 428–432. Springer, Heidelberg (1996)
Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Cimatti, A., Roveri, M., Tchaltsev, A.: Manual for property realizability tool, Prosyd Delivarable D1.2/8 (December 2006), http://www.prosyd.org
Kurshan, R.: Computer-Aided Verification of Coordinating Processes: the automata theoretic approach. Princeton University Press, Princeton, NJ (1994)
Pill, I., Semprini, S., Cavada, R., Roveri, M., Bloem, R., Cimatti, A.: Formal analysis of hardware requirements. In: Design Automation Conference, pp. 821–826 (2006)
Piterman, N., Pnueli, A., Sa’ar, 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)
Wiegers, K.E.: Inspecting requirements. StickyMinds Weekly Colum (July 2001)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bloem, R., Cavada, R., Pill, I., Roveri, M., Tchaltsev, A. (2007). RAT: A Tool for the Formal Analysis of Requirements. In: Damm, W., Hermanns, H. (eds) Computer Aided Verification. CAV 2007. Lecture Notes in Computer Science, vol 4590. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73368-3_30
Download citation
DOI: https://doi.org/10.1007/978-3-540-73368-3_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73367-6
Online ISBN: 978-3-540-73368-3
eBook Packages: Computer ScienceComputer Science (R0)