Abstract
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 requirements specifications (as found in practice) and formal ones (as needed in formal methods). The user is supported by an interactive syntax-directed editor, parsers and linearizers. As a formal specification language we realize the Object Constraint Language, a substandard of the UML, on the informal side a fragment of English. The implementation is based on the Grammatical Framework, a generic tool that combines linguistic and logical methods.
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
W. Ahrendt, T. Baar, B. Beckert, M. Giese, E. Habermalz, R. Hähnle, W. Menzel, and P. H. Schmitt. The KeY approach: Integrating object oriented design and formal verification. In M. Ojeda-Aciego, I. P. de Guzmán, G. Brewka, and L. M. Pereira, editors, Proc. JELIA, LNAI 1919, pages 21–36. Springer, 2000.
M. Carlsson and T. Hallgren. Fudgets—Purely Functional Processes with applications to Graphical User Interfaces. PhD thesis, Department of Computing Science, Chalmers University of Technology, 1998.
Y. Coscoy, G. Kahn, and L. Thery. Extracting text from proofs. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proc. Second Int. Conf. on Typed Lambda Calculi and Applications, volume 902 of LNCS, pages 109–123, 1995.
M. Dymetman, V. Lux, and A. Ranta. XML and multilingual document authoring: Convergent trends. In COLING, Saarbrücken, Germany, pages 243–249, 2000.
T. Hallgren and A. Ranta. An extensible proof text editor. In M. Parigot and A. Voronkov, editors, Logic for Programming and Automated Reasoning, LPAR, LNAI 1955, pages 70–84. Springer, 2000.
R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. JACM, 40(1):143–184, 1993.
A. Holt and E. Klein. A semantically-derived subset of English for hardware verification. In Proc. Ann. Meeting Ass. for Comp. Ling., pages 451–456, 1999.
H. Hussmann, B. Demuth, and F. Finger. Modular architecture for a toolset supporting OCL. In A. Evans, S. Kent, and B. Selic, editors, Proc. 3rd Int. Conf. on the Unified Modeling Language, LNCS 1939, pages 278–293. Springer, 2000.
D. Jackson. Alloy: A lightweight object modelling notation. http://sdg.lcs.mit.edu/~dnj/pubs/alloy-journal.pdf, July 2000.
R. Kramer. iContract—the Java Designs by Contract tool. In Proc. Technology of OO Languages and Systems, TOOLS 26. IEEE CS Press, Los Alamitos, 1998.
G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06i, Iowa State Univ., Dept. of Computer Science, Feb. 2000.
K. R. M. Leino, G. Nelson, and J. B. Saxe. ESC/Java user’s manual. Technical Note #2000-002, Compaq Systems Research Center, Palo Alto, USA, May 2000.
B. Nordström, K. Petersson, and J. M. Smith. Martin-löf’s type theory. In S. Abramasky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 5. Oxford University Press, 2000.
Object Modeling Group. Response to the UML 2.0 OCL RfP, Aug. 2001. http://cgi.omg.org/cgi-bin/doc?ad/01-08-01.
Object Modeling Group. Unified Modelling Language Specification, version 1.4, Sept. 2001. http://www.omg.org/cgi-bin/doc?formal/01-09-67.
R. Power and D. Scott. Multilingual authoring using feedback texts. In COLINGACL 98, Montreal, Canada, 1998.
A. Ranta. Type Theoretical Grammar. Oxford University Press, 1994.
A. Ranta. Grammatical framework homepage, 2000. http://www.cs.chalmers.se/~aarne/GF/index.html.
T. Teitelbaum and T. Reps. The Cornell program synthesizer: A syntax-directed programming environment. CACM, 24(9):563–573, 1981.
Unisys Corp. et al. XML Metadata Interchange (XMI), Oct. 1998. ftp://ftp.omg.org/pub/docs/ad/98-10-05.pdf.
J. Warmer and A. Kleppe. The Object Constraint Language: Precise Modelling with UML. Addison-Wesley, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hähnle, R., Johannisson, K., Ranta, A. (2002). An Authoring Tool for Informal and Formal Requirements Specifications. In: Kutsche, RD., Weber, H. (eds) Fundamental Approaches to Software Engineering. FASE 2002. Lecture Notes in Computer Science, vol 2306. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45923-5_16
Download citation
DOI: https://doi.org/10.1007/3-540-45923-5_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43353-8
Online ISBN: 978-3-540-45923-1
eBook Packages: Springer Book Archive