Abstract
This paper describes the development, verification and model-based validation of a safety-critical pressure relief function for a digital hydraulic system. It demonstrates techniques to handle typical challenges that are encountered when verifying and validating cyber-physical systems with complex dynamical behaviour. The system is developed using model-based design in Simulink. The verification part focuses on verification of functional properties of the controller, where formal automated verification tools are employed. The validation part focuses on validating that the controller has the desired impact on the physical system. In the latter part search-based methods are used to find undesired behaviour in a simulation model of the system. The combination of techniques provides confidence in the resilience of the developed system.
Work funded by the DiHy project in the EFFIMA program coordinated by Fimecc and the EDiHy project (no. 140003) funded by the Academy of Finland.
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baresel, A., Pohlheim, H., Sadeghipour, S.: Structural and functional sequence test of dynamic and state-based software with evolutionary algorithms. In: Cantú-Paz, E., et al. (eds.) GECCO 2003. LNCS, vol. 2724, pp. 2428–2441. Springer, Heidelberg (2003)
Boström, P.: Contract-based verification of simulink models. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 291–306. Springer, Heidelberg (2011)
Boström, P., Björkqvist, J.: Detecting design flaws in control systems using optimisation methods. In: CACSD 2006, pp. 1544–1549. IEEE (2006)
Boström, P., Grönblom, R., Huotari, T., Wiik, J.: An approach to contract-based verification of Simulink models. Tech. Rep. 985, Turku Centre for Computer Science, TUCS (2010)
Cofer, D.: Model checking: Cleared for take off. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 76–87. Springer, Heidelberg (2010)
de Moura, L., 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)
Etienne, J.F., Fechter, S., Juppeaux, E.: Using Simulink Design Verifier for proving behavioral properties on a complex safety critical system in the ground transportation domain. In: Aiguier, M., Bretaudeau, F., Krob, D. (eds.) CSDM 2010. Springer (2010)
Ketonen, M., Huova, M., Heikkilä, M., Linjama, M., Boström, P., Waldén, M.: Digital hydraulic pressure relief function. In: Plummer, A.R. (ed.) FPMC 2012 (2012)
Lillås, K.: Global optimization algorithms in hydraulic controller testing. Master’s thesis, Åbo Akademi University (2008)
Linjama, M., Koskinen, K.T., Vilenius, M.: Accurate tracking control of water hydraulic cylinder with non-ideal on/off valves. International Journal of Fluid Power 4, 7–16 (2003)
Linjama, M., Vilenius, M.: Digital hydraulics - towards perfect valve technology. In: Vilenius, J., Koskinen, K.T. (eds.) SICFP 2007. Tampere University of Technology (2007)
Maraninchi, F., Morel, L.: Logical-time contracts for reactive embedded components. In: 30th EUROMICRO Conference on Component-Based Software Engineering Track, ECBSE 2004. IEEE (2004)
Mathworks Inc.: Simulink (2014), http://www.mathworks.com/products/simulink
Miller, S.P., Anderson, E.A., Wagner, L.G., Wahlen, M.W., Heimdahl, M.P.E.: Formal verification of flight critical software. In: AIAA Guidance, Navigation and Control Conference and Exhibit. AIAA (2005)
Monniaux, D.: The pitfalls of verifying floating-point computations. ACM Transactions on Programming Languages and Systems 30(3) (2008)
Mosterman, P.J., Zander, J., Hamon, G., Denckla, B.: A computational model of time for stiff hybrid systems applied to control synthesis. Control Engineering Practice 20(1) (2012)
Murphy, B., Wakefield, A., Friedman, J.: Best practices for verification, validation, and test in model-based design. Tech. Rep. 2008-01-1469, Mathworks (2008)
Platzer, A., Quesel, J.-D.: KeYmaera: A hybrid theorem prover for hybrid systems (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171–178. Springer, Heidelberg (2008)
Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt Jr., W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)
Wiik, J., Boström, P.: Contract-based verification of MATLAB and simulink matrix-manipulating code. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 396–412. Springer, Heidelberg (2014)
Zhan, Y.: A Search-Based Framework for Automatic Test-Set Generation for MATLAB/Simulink Models. Ph.D. thesis, University of York, UK (2006)
Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Stateflow/Simulink verification. Formal Methods in System Design 43 (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Boström, P., Heikkilä, M., Huova, M., Waldén, M., Linjama, M. (2014). Verification and Validation of a Pressure Control Unit for Hydraulic Systems. In: Majzik, I., Vieira, M. (eds) Software Engineering for Resilient Systems. SERENE 2014. Lecture Notes in Computer Science, vol 8785. Springer, Cham. https://doi.org/10.1007/978-3-319-12241-0_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-12241-0_8
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-12240-3
Online ISBN: 978-3-319-12241-0
eBook Packages: Computer ScienceComputer Science (R0)