Abstract
Precise documentation of requirements is important for developing and certifying mission critical software. We specify cyber-physical systems via an Event-B-like machine which declar es the monitored and controlled variables and their initial condition. A machine event models the joint action of the plant and the controller. Embedded in the event action is a function table that specifies the input-output behaviour of the controller, as monitored variables are periodically updated by the plant. We extend the Event-B notation with queries and modules. The resulting machine provides us with a mathematical description of the overall system behaviour, thus allowing us to validate the requirements by proving that (1) the input-output specification of the controller is complete, disjoint and well-defined, and that (2) the machine satisfies system-wide consistency invariants elicited from domain experts. A biomedical device is used as a case study, and we mechanize proofs via a SMT solver.
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
Notes
- 1.
Section 5.3.3.2 of IEEE-181: “If there is more than one reference level instant, the reference level closest to the 50 % reference level instance (see 5.3.3.1) is used, unless otherwise specified.” Obviously \(t90p-t10p < 0\) represents an unusual waveform. Nevertheless, the software must deal with all inputs, however unusual.
- 2.
Equations 5 and 6 on page 20 of IEEE-181 provide the interpolation formulas.
- 3.
See the post-condition of query \( seq\mathrm 2 rfun \). Given a real \(t\) and a natural number \(n\), \(\lfloor t+n \rfloor = \lfloor t \rfloor + n\). Thus \(\lfloor t+1 \rfloor = \lfloor t \rfloor + 1\). In the definition of \( seq\mathrm 2 rfun (s)(t)\) the coefficients always add up to one, i.e. \((\lfloor t+1\rfloor -t) + (t-\lfloor t\rfloor ) = 1\). This eliminates the possibility of division by zero and avoids the case analysis in the IEEE-181 standard. Both \(swf\) and \( seq\mathrm 2 rfun (swf)\) agree on their projected levels from the integer domain of \(swf\), i.e. \(swf = {\mathbb {N}}\mathbin \lhd seq\mathrm 2 rfun (swf)\).
- 4.
For the complete definition of type \(SEQ[G] \triangleq (\bigcup \nolimits n : {\mathbb {N}}\, \bullet 1..n \mathbin \rightarrow G)\) that supports the standard queries \(count\), \(has\), \(head\), and \(tail\), see our extended report [18].
References
Abrial, J.-R.: Modeling in Event-B. Cambridge University Press, New York (2010)
Abrial, J.-R., Mussat, L.: On using conditional definitions in formal theories. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 242–269. Springer, Heidelberg (2002)
de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Eles, C., Lawford, M.: A tabular expression toolbox for matlab/simulink. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 494–499. Springer, Heidelberg (2011)
Gunter, C.A., Gunter, E.L., Jackson, M., Zave, P.: A reference model for requirements and specifications. IEEE Softw. 17(3), 37–43 (2000)
Hatcliff, J., Leavens, G.T., Leino, K.R.M., Müller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1–16:58 (2012)
IEEE: IEEE standard for transitions, pulses, and related waveforms. IEEE Std 181-2011 (Revision of IEEE Std 181-2003), pp. 1–71 (2011)
Jackson, M.: Software Requirements Specifications: A Lexicon of Practice, Principles and Prejudices. Addison-Wesley, New York (1995)
Jackson, M.: The operational principle and problem frames. Reflections on the Work of C. A. R. Hoare. Springer, London (2010)
Jin, Y., Parnas, D.L.: Defining the meaning of tabular mathematical expressions. Sci. Comput. Program. 75(11), 980–1000 (2010)
Lawford, M., Froebel, P., Moum, G.: Application of tabular methods to the specification and verification of a nuclear reactor shutdown system. Formal Meth. Syst. Des. (2000). http://www.cas.mcmaster.ca/~lawford/papers/FMSD.html
Maamria, I., Butler, M.: Rewriting and well-definedness within a proof system. EPTCS 43, 49–64 (2010)
Maibaum, T.S.E., Wassyng, A.: A product-focused approach to software certification. IEEE Comput. 41(2), 91–93 (2008)
Meyer, B.: Object-Oriented Software Construction. Prentice Hall, New Jersey (1997)
Misra, J.: A Discipline of Multiprogramming: Programming Theory for Distributed Applications. Springer, New York (2001)
Ostroff, J.S., Paige, R.F.: The logic of software design. Proc. IEE - Softw. 147(3), 72–80 (2000)
Ostroff, J.S., Wang, C.-W., Hudon, S.: Precise documentation of requirements and executable specifications. Technical Report CSE-2012-03, York University (2012)
Ostroff, J.S., Wang, C.-W., Hudon, S.: Precise documentation and validation of requirements. Technical Report CSE-2013-08, York University (2013)
Parnas, D.L.: Predicate logic for software engineering. IEEE Trans. Softw. Eng. 19(9), 856–862 (1993)
Parnas, D.L., Madey, J.: Functional documentation for computer systems. Sci. Comput. Prog. 25, 41–61 (1995)
Wassyng, A., Lawford, M.: Lessons learned from a successful implementation of formal methods in an industrial project. In: FME, pp. 133–153 (2003)
Wassyng, A., Lawford, M.: Software tools for safety-critical software development. STTT 8(4–5), 337–354 (2006)
Wassyng, A., Lawford, M., Hu, X.: Timing tolerances in safety-critical software. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 157–172. Springer, Heidelberg (2005)
Acknowledgments
The authors would like to thank NSERC and ORF for their generous financial support.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Wang, CW., Ostroff, J.S., Hudon, S. (2014). Precise Documentation and Validation of Requirements. In: Artho, C., Ölveczky, P. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2013. Communications in Computer and Information Science, vol 419. Springer, Cham. https://doi.org/10.1007/978-3-319-05416-2_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-05416-2_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-05415-5
Online ISBN: 978-3-319-05416-2
eBook Packages: Computer ScienceComputer Science (R0)