Abstract
As the reliability and safety of a system become more important, we need the requirement specification that is clear to read and has no error. So far several approaches have been proposed; the formal modelling technique is one of the effective approaches to get the correct specification. But, in the embedded system field, we cannot expect that the most of system engineers know about the formal specification technique. They are the experts of the system, not the specialist of system or software engineering. In our paper, we provide the new approach to mitigate this problem. The user uses only the natural language, and a tool provides the check the text on the fly and points out the sentence that has a problem. The formal model is constructed in the background. The user doesn’t need to know the description of the formal model. In this paper, we introduce this approach and the tool, Cardion.spec that we implement our idea.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Sikora, E., Tenbergen, B., Pohl, K.: Industry needs and research directions in requirements engineering for embedded systems. Requirements Eng. 17(1), 57–78 (2012)
McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press, Cambridge (2015)
IEEE: IEEE Recommended Practice for Software Requirements Specification (IEEE Std 830-1998). IEEE (1998)
Ott, D.: Automatic requirement categorization of large natural language specifications at Mercedes-Benz for review improvements. In: Doerr, J., Opdahl, A.L. (eds.) REFSQ 2013. LNCS, vol. 7830, pp. 50–64. Springer, Heidelberg (2013)
Ott, D., Raschke, A.: Review improvement by requirements classification at Mercedes-Benz: limits of empirical studies in educational environments. In: 2012 IEEE Second International Workshop on Empirical Requirements Engineering (EmpiRE). IEEE (2012)
ISO/IEC, ISO/IEC 13568:2002: Information technology – Z formal specification notation – Syntax, type system and semantics, ISO (2002)
Boulanger, J.-L.: Industrial Use of Formal Methods: Formal Verification. Wiley, New York (2013)
Iordache, O.: Methods. In: Iordache, O. (ed.) Polystochastic Models for Complexity. UCS, vol. 4, pp. 17–61. Springer, Heidelberg (2010)
Heitmeyer, C.L., Jeffords, R.D., Labaw, B.G.: Automated consistency checking of requirements specifications. ACM Trans. Softw. Eng. Methodol. (TOSEM) 5(3), 231–261 (1996)
Barnes, J.: Programming in Ada 2012. Cambridge University Press, Cambridge (2014)
Parnas, D.L., Madey, J.: Functional documentation for computer systems engineering: version 2. McMaster University, Faculty of Engineering, Communications Research Laboratory (1991)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Appendix
Appendix
A user writes the specification in the natural language (Fig. 6, left). Cardion.spec creates the SPARK codes (Fig. 6, upper right) and FSM model (Fig. 6, lower down) internally. The user does not need to see those representations, could focus on the natural language text.
Cardion.spec tool image
But we could use the SPARK codes for the validation purpose.
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Ito, M. (2016). Cardion.spec: An Approach to Improve the Requirements Specification Written in the Natural Language Through the Formal Method. In: Kreiner, C., O'Connor, R., Poth, A., Messnarz, R. (eds) Systems, Software and Services Process Improvement. EuroSPI 2016. Communications in Computer and Information Science, vol 633. Springer, Cham. https://doi.org/10.1007/978-3-319-44817-6_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-44817-6_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-44816-9
Online ISBN: 978-3-319-44817-6
eBook Packages: Computer ScienceComputer Science (R0)