Abstract
Low cost embedded cyber-physical systems and ubiquitous networking have opened up a new world of connected devices in our homes and workplaces, and in safety critical contexts such as automobiles, medical care, and drone-based air vehicles. There are many different approaches to developing and assuring these systems, but not all take a rigorous approach and even fewer offer integrated assurance frameworks.
In this STRESS 2018 tutorial, we introduce students to an integrated modeling and verification environment for high-assurance embedded systems based on the Sireum translation, analysis, and verification platform from Kansas State University. Sireum includes a programming language called Slang for developing high-assurance embedded applications and a verification framework called Logika that uses symbolic execution technology to provide highly automated and easy-to-use software contract checking capabilities. Slang and Logika align with the Architecture and Analysis Definition Language (AADL) for architecture modeling and component interface declarations, analysis of AADL models, and configuration of execution platforms using standard AADL properties. AADL component behavioral properties can be specified and verified using, for example, the Behavioral Language for Embedded Systems with Software (BLESS).
This work is sponsored in part by US National Science Foundation Food and Drug Administration Scholar-in-Residence program (CNS 1238431,1355778,1446544,1565544), the Department of Homeland Security (DHS) Science and Technology Directorate, Homeland Security Advanced Research Projects Agency (HSARPA), Cyber Security Division (DHS S&T/HSARPA/CDS) BAA HSHQDC- 14-R-B0005, the Government of Israel and the National Cyber Bureau in the Government of Israel via contract number D16PC00057.
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
Carpenter, T., Hatcliff, J., Vasserman, E.Y.: A reference separation architecture for mixed-criticality medical and IoT devices. In: Proceedings of the 1st ACM Workshop on the Internet of Safe Things, SafeThings 2017, New York, pp. 14–19. ACM (2017)
Deng, X., Robby, Hatcliff, J.: Kiasan/KUnit: automatic test case generation and analysis feedback for open object-oriented systems. In: Testing: Academic and Industrial Conference Practice and Research Techniques - MUTATION (TAICPART-MUTATION 2007), pp. 3–12, September 2007
Feiler, P.H., Hansson, J., de Niz, D., Wrage, L.: System architecture virtual integration: an industrial case study. Technical report CMU/SEI-2009-TR-017, CMU (2009)
Harp, S., Carpenter, T., Hatcliff, J.: A reference architecture for secure medical devices. Biomed. Instrum. Technol. 52(5), 357–365 (2018). Association for the Advancement of Medical Instrumentation (AAMI)
Hatcliff, J., Dwyer, M.B., Robby: Bogor: a flexible framework for creating software model checkers. In: Testing: Academic Industrial Conference - Practice And Research Techniques (TAIC PART 2006), pp. 3–22, August 2006
Hatcliff, J., Robby, Chalin, P., Belt, J.: Explicating symbolic execution (xSymExe): an evidence-based verification framework. In: 35th International Conference on Software Engineering (ICSE), pp. 222–231, May 2013
Hatcliff, J., Larson, B., Carpenter, T., Jones, P., Zhang, Y., Jorgens, J.: The Open PCA pump project: an exemplar open source medical device as a community resource. In: Proceedings of the 2018 Medical Cyber-Physical Systems (MedCPS) Workshop (2018)
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)
Hatcliff, J., Wassyng, A., Kelly, T., Comar, C., Jones, P.L.: Certifiably safe software-dependent systems: challenges and directions. In: Proceedings of the on Future of Software Engineering (ICSE FOSE), pp. 182–200 (2014)
SAE International: SAE AS5506 Rev. C Architecture Analysis and Design Language (AADL). SAE International (2017). http://www.sae.org
King, A.L., et al.: Towards assurance for plug & play medical systems. In: Koornneef, F., van Gulijk, C. (eds.) SAFECOMP 2014. LNCS, vol. 9337, pp. 228–242. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24255-2_17
Larson, B., Hatcliff, J., Fowler, K., Delange, J.: Illustrating the AADL error modeling annex (v.2) using a simple safety-critical medical device. In: Proceedings of the 2013 ACM SIGAda Annual Conference on High Integrity Language Technology, HILT 2013, New York, pp. 65–84. ACM (2013)
Larson, B.R., Chalin, P., Hatcliff, J.: BLESS: formal specification and verification of behaviors for embedded systems with software. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 276–290. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38088-4_19
Larson, B.R., Hatcliff, J., Chalin, P.: Open source patient-controlled analgesic pump requirements documentation. In: Proceedings of the 5th International Workshop on Software Engineering in Health Care, Piscataway, pp. 28–34. IEEE (2013)
Larson, B.R., Zhang, Y., Barrett, S.C., Hatcliff, J., Jones, P.L.: Enabling safe interoperation by medical device virtual integration. IEEE Des. Test 32, 74–88 (2015)
Lee, I., et al.: Challenges and research directions in medical cyber-physical systems. Proc. IEEE 100(1), 75–90 (2012)
Leroy, X., Blazy, S., Kästner, D., Schommer, B., Pister, M., Ferdinand, C.: CompCert - a formally verified optimizing compiler. In: ERTS 2016: Embedded Real Time Software and Systems. SEE (2016)
Procter, S., Hatcliff, J.: An architecturally-integrated, systems-based hazard analysis for medical applications. In: Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 124–133. IEEE (2014)
Robby, Dwyer, M.B., Hatcliff, J.: Bogor: an extensible and highly-modular software model checking framework. In: Proceedings of the 9th European Software Engineering Conference Held Jointly with 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC/FSE-2011, pp. 267–276 (2003)
Kansas State University: Open PCA pump project (2018). http://openpcapump.santoslab.org
Zhang, Y., Larson, B., Hatcliff, J.: Assurance case considerations for interoperable medical systems. In: Gallina, B., Skavhaug, A., Schoitsch, E., Bitsch, F. (eds.) SAFECOMP 2018. LNCS, vol. 11094, pp. 42–48. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99229-7_5
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Robby, Hatcliff, J., Belt, J. (2018). Model-Based Development for High-Assurance Embedded Systems. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Modeling. ISoLA 2018. Lecture Notes in Computer Science(), vol 11244. Springer, Cham. https://doi.org/10.1007/978-3-030-03418-4_32
Download citation
DOI: https://doi.org/10.1007/978-3-030-03418-4_32
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-03417-7
Online ISBN: 978-3-030-03418-4
eBook Packages: Computer ScienceComputer Science (R0)