Abstract
In designing systems, engineers decompose the problem into smaller, more manageable tasks. A classic example of this is the separation principle from control systems which allows one to decompose the design of an optimal feedback control system into two independent tasks by designing (a) an observer, and (b) a controller. We investigate an analogous result for embedded system interfacing that will allow separation of the design of the input and output hardware interfaces while still guaranteeing the ability of the software to meet the system requirements. We define the notions of observability (controllability) of the system requirements with respect to the input (output) interface. We show that for a system that can be modeled by a functional four-variable model, observability and controllability allow for the separation of the design of the input and output interfaces. We also show that this separation is not always possible for systems that need the general, relational four-variable model. By strengthening either observability or controllability, we restrict the choice of input or output interfaces, but ensure separability of their designs.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Brink, C., Kahl, W., Schmidt, G. (eds.): Relational Methods in Computer Science. Advances in Computing. Springer (1997)
Desharnais, J., Mili, A., Nguyen, T.: Refinement and Demonic Semantics. In: Brink, et al. (eds.) [1], ch. 11, pp. 166–183 (1997)
Faulk, S., Finneran, J., Kirby, J., Shash, S., Sutton, J.: Experience applying the CoRE method to the Lockhead C-130J software requirements. In: Ninth Annual Conference on Computer Assurance, Gaithersburg, Maryland (June 1994)
Frappier, M.: A Relational Basis for Program Construction by Parts. Ph.D. thesis, Computer Science Department, University of Ottawa (1995)
Joseph, D.P., Tou, T.J.: On linear control theory. Transactions of the American Institute of Electrical Engineers. Part II: Applications and Industry 80(4), 193–196 (1961)
Kahl, W.: Refinement and development of programs from relational specifications. Electronic Notes in Theoretical Computer Science (ENTCS) 44(3), 51–93 (2003)
Kalman, R.E.: Contributions to the theory of optimal control. Bol. Soc. Mat. Mexicana 5(2), 102–119 (1960)
Lawford, M., McDougall, J., Froebel, P., Moum, G.: Practical application of functional and relational methods for the specification and verification of safety critical software. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 73–88. Springer, Heidelberg (2000)
Lempia, D.L., Miller, S.P.: Requirements engineering management handbook. Tech. Rep. DOT/FAA/AR-08/32, U.S. Department of Transportation, Federal Aviation Administration (June 2009)
Parnas, D.L.: On the criteria to be used in decomposing systems into modules. Communications of the ACM 15(12), 1053–1058 (1972)
Parnas, D.L., Madey, J.: Functional documents for computer systems. Science of Computer Programming 25(1), 41–61 (1995)
Patcas, L.M., Lawford, M., Maibaum, T.: From system requirements to software requirements in the four-variable model. In: Schneider, S., Treharne, H., Margaria, T., Padberg, J., Taentzer, G. (eds.) Proceedings of the Automated Verification of Critical Systems (AVoCS 2013). Electronic Communications of the EASST, vol. 66 (2014)
Thompson, J., Heimdahl, M., Miller, S.P.: Specification-based prototyping for embedded systems. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC/FSE 1999. LNCS, vol. 1687, pp. 163–179. Springer, Heidelberg (1999)
Van Schouwen, A.: The A-7 requirements model: Re-examination for real-time systems and an application to monitoring systems. Tech. Rep. 90-276, Queens University, Ontario, Canada (1990)
Wassyng, A., Lawford, M.: Lessons learned from a successful implementation of formal methods in an industrial project. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 133–153. Springer, Heidelberg (2003)
Wonham, W.M.: Lecture notes on supervisory control of discrete-event systems. Systems Control Group, Department of Electrical & Computer Engineering, University of Toronto (July 2013), http://www.control.toronto.edu/DES/
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
Patcas, L.M., Lawford, M., Maibaum, T. (2014). A Separation Principle for Embedded System Interfacing. In: Albert, E., Sekerinski, E. (eds) Integrated Formal Methods. IFM 2014. Lecture Notes in Computer Science(), vol 8739. Springer, Cham. https://doi.org/10.1007/978-3-319-10181-1_23
Download citation
DOI: https://doi.org/10.1007/978-3-319-10181-1_23
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10180-4
Online ISBN: 978-3-319-10181-1
eBook Packages: Computer ScienceComputer Science (R0)