{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T14:44:02Z","timestamp":1725806642230},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319122403"},{"type":"electronic","value":"9783319122410"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-12241-0_8","type":"book-chapter","created":{"date-parts":[[2014,10,8]],"date-time":"2014-10-08T11:39:08Z","timestamp":1412768348000},"page":"101-115","source":"Crossref","is-referenced-by-count":2,"title":["Verification and Validation of a Pressure Control Unit for Hydraulic Systems"],"prefix":"10.1007","author":[{"given":"Pontus","family":"Bostr\u00f6m","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mikko","family":"Heikkil\u00e4","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mikko","family":"Huova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marina","family":"Wald\u00e9n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matti","family":"Linjama","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2428","DOI":"10.1007\/3-540-45110-2_147","volume-title":"Genetic and Evolutionary Computation - GECCO 2003","author":"A. Baresel","year":"2003","unstructured":"Baresel, A., Pohlheim, H., Sadeghipour, S.: Structural and functional sequence test of dynamic and state-based software with evolutionary algorithms. In: Cant\u00fa-Paz, E., et al. (eds.) GECCO 2003. LNCS, vol.\u00a02724, pp. 2428\u20132441. Springer, Heidelberg (2003)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-642-24559-6_21","volume-title":"Formal Methods and Software Engineering","author":"P. Bostr\u00f6m","year":"2011","unstructured":"Bostr\u00f6m, P.: Contract-based verification of simulink models. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol.\u00a06991, pp. 291\u2013306. Springer, Heidelberg (2011)"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Bostr\u00f6m, P., Bj\u00f6rkqvist, J.: Detecting design flaws in control systems using optimisation methods. In: CACSD 2006, pp. 1544\u20131549. IEEE (2006)","DOI":"10.1109\/CACSD.2006.285488"},{"key":"8_CR4","unstructured":"Bostr\u00f6m, P., Gr\u00f6nblom, R., Huotari, T., Wiik, J.: An approach to contract-based verification of Simulink models. Tech. Rep. 985, Turku Centre for Computer Science, TUCS (2010)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-16164-3_6","volume-title":"Model Checking Software","author":"D. Cofer","year":"2010","unstructured":"Cofer, D.: Model checking: Cleared for take off. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol.\u00a06349, pp. 76\u201387. Springer, Heidelberg (2010)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1007\/978-3-642-15654-0_4"},{"key":"8_CR8","unstructured":"Ketonen, M., Huova, M., Heikkil\u00e4, M., Linjama, M., Bostr\u00f6m, P., Wald\u00e9n, M.: Digital hydraulic pressure relief function. In: Plummer, A.R. (ed.) FPMC 2012 (2012)"},{"key":"8_CR9","unstructured":"Lill\u00e5s, K.: Global optimization algorithms in hydraulic controller testing. Master\u2019s thesis, \u00c5bo Akademi University (2008)"},{"key":"8_CR10","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1080\/14399776.2003.10781151","volume":"4","author":"M. Linjama","year":"2003","unstructured":"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\u00a04, 7\u201316 (2003)","journal-title":"International Journal of Fluid Power"},{"key":"8_CR11","unstructured":"Linjama, M., Vilenius, M.: Digital hydraulics - towards perfect valve technology. In: Vilenius, J., Koskinen, K.T. (eds.) SICFP 2007. Tampere University of Technology (2007)"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1109\/EURMIC.2004.1333355"},{"key":"8_CR13","unstructured":"Mathworks Inc.: Simulink (2014), \n                    \n                      http:\/\/www.mathworks.com\/products\/simulink"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.2514\/6.2005-6431"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: The pitfalls of verifying floating-point computations. ACM Transactions on Programming Languages and Systems 30(3) (2008)","DOI":"10.1145\/1353445.1353446"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"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\u00a020(1) (2012)","DOI":"10.1016\/j.conengprac.2011.04.013"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Murphy, B., Wakefield, A., Friedman, J.: Best practices for verification, validation, and test in model-based design. Tech. Rep. 2008-01-1469, Mathworks (2008)","DOI":"10.4271\/2008-01-1469"},{"key":"8_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A. Platzer","year":"2008","unstructured":"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.\u00a05195, pp. 171\u2013178. Springer, Heidelberg (2008)"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt Jr., W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1007\/978-3-319-11737-9_26","volume-title":"ICFEM 2014","author":"J. Wiik","year":"2014","unstructured":"Wiik, J., Bostr\u00f6m, P.: Contract-based verification of MATLAB and simulink matrix-manipulating code. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol.\u00a08829, pp. 396\u2013412. Springer, Heidelberg (2014)"},{"key":"8_CR21","unstructured":"Zhan, Y.: A Search-Based Framework for Automatic Test-Set Generation for MATLAB\/Simulink Models. Ph.D. thesis, University of York, UK (2006)"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Stateflow\/Simulink verification. Formal Methods in System Design\u00a043 (2013)","DOI":"10.1007\/s10703-013-0195-3"}],"container-title":["Lecture Notes in Computer Science","Software Engineering for Resilient Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12241-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T02:24:19Z","timestamp":1559010259000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-12241-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319122403","9783319122410"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12241-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}