Model-Based Development for High-Assurance Embedded Systems
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
- PDF / 1,754,096 Bytes
- 7 Pages / 439.37 x 666.142 pts Page_size
- 101 Downloads / 212 Views
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).
1
Overview
Figure 1 shows our approach to critical system development and assurance that emphasizes the use of formally specified architectures as the “scaffolding” through which many different activities are organized and synchronized. A key theme of our approach is the deep integration of architectural models and programming leading to the following features: 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. c Springer Nature Switzerland AG 2018 T. Margaria and B. Steffen (Eds.): ISoLA 2018, LNCS 11244, pp. 539–545, 2018. https://doi.org/10.1007/978-3-030-03418-4_32
540
Robby et al.
Fig. 1. Approach overview
– component code skeletons and realization of communication between components are automatically generated from architectural models, leading to strong traceability between models and deployed executables, – configuration of underlying platform aspects including real-time threading policies and communication quality-of-service policies that are often specified at the programming language level are instead specified at the modeling level, – analyses shift freely between the different abstraction levels provided by models and conventional programming languages. The modeling approach is based on the SAE standard Architecture Analysis and Definition Language (AADL) [10]. AADL supports
Data Loading...
