The Architecture Analysis Design Language (AADL) is an architecture description language for design of cyber-physical systems–machines controlled by software. The AADL standard, SAE International AS5506D, describes Run-Time Services (RTS) to be provided to execute AADL models in accordance with semantics defined by the standard. The RTS of primary concern are transport services and timing services. Although, the study presented in [1] sets a foundation for the formal semantics of AADL, but without modeling time. This paper extends and simplifies this formalization using a modal logic defined by a Kripke structure, to explicitly include time. The RTS defined in the AADL standard are also expanded to support reactive state-transition machines of the Behavior Specification annex standard language (BA) and its closely-related, formally-defined counterpart, the Behavior Language for Embedded Systems with Software (BLESS). An example of AADL RTS with time, implemented by the High Assurance Modeling and Rapid Engineering for Embedded Systems (HAMR) for state-transition machine behavior written in BLESS, is also presented.

Safety-critical cyber-physical systems require evidence they are indeed safe. In practice, such evidence is results of system tests. Unfortunately, tests can only demonstrate the presence of software errors, not their absence, and can practically cover a tiny fraction of system state space. Valiant efforts to formally verify program correctness have either been excruciatingly difficult (theorem proving) or incomplete (static analysis, model checking, SAT or SMT solving). The BLESS Methodology was created specifically for engineers in industry to formally verify software controlling machines. The BLESS Methodology transforms programs that control machines, annotated with assertions to form proof outlines, into deductive proofs that every possible program execution will conform to its specification. To the extent that cyber-physical system specifications have been validated to express system safety and performance, a deductive proof can be a convincing argument to a person of program correctness. This paper uses a simple safety-critical system to argue that behavior correctness proof under the BLESS Methodology is a convincing verification artifact in addition to customary testing.

The Architecture Analysis and Design Language (AADL) is a SAE standard for modeling both hardware and software architecture of embedded systems. Widely embraced by stakeholders in critical real-time embedded systems, the AADL standard is used to address a large set of concerns including performances (latency, schedulability), safety, and security. The ADEPT workshop aims to present and report on current projects in the field of design, implementation, and verification of critical real-time embedded systems where AADL is a first-citizen technology. This article is a summary of the second edition of the workshop in 2023.

The Internet of Medical Things (IoMT) represents a specialized domain within the Internet of Things, focusing on medical devices that require regulatory approval to ensure patient safety. Trusted composition of IoMT systems aims to ensure high assurance of the entire composed system, despite potential variability in the assurance levels of individual components. Achieving this trustworthiness in IoMT systems, especially when using less-assured, commercial, off-the-shelf networks like Ethernet and WiFi, presents a significant challenge. To address this challenge, this paper advocates a systematic approach that leverages the Architecture Analysis & Design Language (AADL) along with Behavior Language for Embedded Systems with Software (BLESS) specification and implementation. This approach aims to provide high assurance on critical components through formal verification, while using less-assured components in a manner that maintains overall system determinism and reliability. A clinical case study involving an automated opioid infusion monitoring IoMT system is presented to illustrate the application of the proposed approach. Through this case study, the effectiveness of the systemic approach in achieving trusted composition of heterogeneous medical devices over less-assured networks is demonstrated.

Risk management is a key part of the development of medical devices to achieve acceptable product safety and pass regulatory scrutiny. As model-based development (MBD) techniques gain ground in the medical device industry, the medical device industry needs guidelines on the best practices of integrating risk management principles and activities in MBD-driven product development. In this paper, we demonstrate how the SAE standard Architecture, Analysis, and Definition Language (AADL) and its Error Modeling (EM) annex can be applied in the development of an open-source patient-controlled analgesic (PCA) pump to support the risk management tasks of ISO 14971 - the primary risk management standard in the medical device domain. While AADL EM has been applied in other domains, our work provides the first mapping of AADL EM to ISO 14971 concepts. It not only represents one of the largest applications to-date of AADL’s EM framework, but also provides the industry and academia an example with considerable complexity to investigate methodologies and methods of integrating MBD and risk management. This work is part of the Open PCA Pump project, which presents a variety of open source integrated development artifacts for a realistic medical device.

Building safe and secure interoperable medical devices with accompanying assurance artifacts is challenging. Many start-up companies have great ideas for innovation, but are not familiar with appropriate safety/security-critical engineering processes, architecture principles, risk management, and assurance techniques. Larger, more experienced, companies may face hurdles in re-engineering their devices for interoperability and greater security. In academia, researchers often have good techniques for addressing some of the issues above, but are not familiar with how a realistic medical device is developed and assured. Building a prototype medical device for a classroom project or research work to validate proposed techniques is often a huge effort. The Open PCA Pump illustrates a full suite of realistic development artifacts including use cases, requirements, architecture models, verified source code, testing and simulation infrastructure, risk management artifacts, and assurance cases that can be used to develop shared understanding of medical device innovations across the academic, industry, and regulatory communities.1

Modern medical devices are increasingly developed by composing a variety of interoperable elements such as medical devices, services, and platform infrastructures. In many scenarios, multi-vendor consortia are organized to support the development and deployment of interoperable medical systems, in which safety-critical element implementations, risk management results, and safety assurance are reused across organizational boundaries. This reality calls for an assurance case approach that supports interfacing, refinement, and composition of distributed, component-level claims and evidences to construct system-level assurance argumentation. We present a collection of objectives and top-level safety claims towards the development of such an approach for interoperable systems built using medical application platforms.

Developing and assuring safety- and security-critical real-time embedded systems is a challenging endeavor that requires many activities applied at multiple levels of abstraction. For these activities to be effective and trustworthy, they must be grounded in a common understanding of the system architecture and behavior. We believe that these activities are best addressed in a unified framework of modeling and programming that enables developers, analysts, and auditors to freely move up and down layers of abstraction, shifting their viewpoints to suit the activities at hand, while maintaining strong traceability across the different layers and views. In this approach, the distinction between “models”, “specifications”, and “programs” is often blurred. In this paper, we summarize an architecture-centric 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. We provide examples of: (a) analyses, behavioral constraints, and implementations, (b) important abstraction transitions, and (c) key traceability relationships within the framework. We discuss how these features are being used to develop systems on time and space partitioned execution and communication platforms for systems in the medical domain. We use an open-source medical device that we are developing – Patient-Controlled Analgesic (PCA) infusion pump as a concrete example.

The complexity of medical devices and the processes by which they are developed pose considerable challenges to producing safe designs and regulatory submissions that are amenable to effective reviews. Designing an appropriate and clearly documented architecture can be an important step in addressing this complexity. Best practices in medical device design embrace the notion of a safety architecture organized around distinct operation and safety requirements. By explicitly separating many safety-related monitoring and mitigation functions from operational functionality, the aspects of a device most critical to safety can be localized into a smaller and simpler safety subsystem, thereby enabling easier verification and more effective reviews of claims that causes of hazardous situations are detected and handled properly. This article defines medical device safety architecture, describes its purpose and philosophy, and provides an example. Although many of the presented concepts may be familiar to those with experience in realization of safety-critical systems, this article aims to distill the essence of the approach and provide practical guidance that can potentially improve the quality of device designs and regulatory submissions.

In system design, an architecture specification or model serves, among other purposes, as a repository to share knowledge about the system being designed. Such a repository enables automatic generation of analytical models for different aspects relevant to system design (timing, reliability, security, etc.). The Architecture Analysis and Design Language (AADL) is a standard proposed by SAE to express architecture specifications and share knowledge between the different stakeholders about the system being designed. To support unambiguous reasoning, formal verification, high-fidelity simulation of architecture specifications in a model-based AADL design workflow, we have defined a formal semantics for the behavior specification of the AADL, the presentation of this semantics is the aim of this paper.

The safe compositionality and integration of heterogeneous components represents a major challenge in medical cyber-physical systems. The paradigm of medical application platforms allows the virtual integration of heterogeneous devices with various communication infrastructures, but does not fully address the safety properties of the overall system. This paper presents a medical device virtual integration framework for composing medical devices and control applications into an interoperable system without violating the safety properties.

Train control systems like most digital controllers are, by definition, hybrid systems as they interact with or try to control some aspects of the physical world. Detailed behavior modeling with constraints specification and formal verification, required for reliability prediction, is a great challenge for hybrid system designers. Train control systems further intensify this challenge with extensive interaction between computing units and their physical environment and their mutual dependence on each other. In this paper, we investigate behavior modeling and formal verification of Chinese Train Control System Level 3 (CTCS-3) using Architectural Analysis & Design Language (AADL) to cope with this challenge. AADL is an architecture description language for embedded systems and is based on model-based engineering paradigm. Along with structural modeling of embedded systems using the core language constructs, AADL also provides support for language extension through annex sublanguages. In system requirements specification document, the behavior of the CTCS-3 is specified as a set of basic operation scenarios that cooperate with each other to achieve safe and secure functionality of trains. Movement Authority (MA) scenario, explored in this paper, is considered as a basic and most crucial scenario to prevent trains from colliding with each other. The detailed discrete behavior of control system is modeled and verified using the Behavior Language for Embedded Systems with Software (BLESS) annex sublanguage of AADL, and the continuous behavior of train with the cyber–physical interaction (communication between train and control system) is modeled using the Hybrid annex sublanguage. The behavior of the MA scenario at system level is verified using the Hybrid Hoare Logic theorem prover. Behavior constraints are specified as assertions using first-order logic formulas augmented with a simple temporal operator.

This paper formally expresses the timing behavior of a cardiac pacemaker as defined in the PACEMAKER System Specification as understood by its principal author. The PACEMAKER System Specification was publicly released by Boston Scientific to provide a real-world subject for application of formal methods in response to Jim Woodcock's request at FM2006 for an industrial Grand Challenge problem. PACEMAKER's use for purposes other than formal methods has been surprising in its variety. Most ambitious is the Software Certification Consortium's mock regulatory submission, PACEMAKER Grand Challenge, to show that a product with safety-critical software is in fact safe. McMaster University is designing a second-generation hardware platform to execute formally-verified software during system feature test validation with an electrical heart simulator to show correct behavior. This paper uses first-order predicates, extended with a simple temporal operator, to formally express what the principal author understands to be "correct" behavior defined in PACEMAKER.

Correct design, and system-level dependability prediction of highly-integrated systems demand the collocation of requirements and architectural artifacts within an integrated development environment. Hybrid systems, having dependencies and extensive interactions between their control portion and their environment, further intensify this need. AADL is a model-based engineering language for the architectural design and analysis of embedded control systems. Core AADL has been extended with a mechanism for discrete behavioral modeling and analysis of control systems, but not for the continuous behavior of the physical environment. In this paper, we introduce a lightweight language extension to AADL called the Hybrid Annex for continuous-time modeling, fulfilling the need for integrated modeling of the computing system along with its physical environment in their respective domains. The Isolette system described in the FAA Requirement Engineering Management Handbook is used to illustrate continuous behavior modeling with the proposed Hybrid Annex.

Correct design, and system-level dependability prediction of highly-integrated systems demand the collocation of requirements and architectural artifacts within an integrated development environment. Hybrid systems, having dependencies and extensive interactions between their control portion and their environment, further intensify this need. AADL is a model-based engineering language for the architectural design and analysis of embedded control systems. Core AADL has been extended with a mechanism for discrete behavioral modeling and analysis of control systems, but not for the continuous behavior of the physical environment. In this paper, we introduce a lightweight language extension to AADL called the Hybrid Annex for continuous-time modeling, fulfilling the need for integrated modeling of the computing system along with its physical environment in their respective domains. The Isolette system described in the FAA Requirement Engineering Management Handbook is used to illustrate continuous behavior modeling with the proposed Hybrid Annex.

This panel brings together designers of both traditional programming languages, and designers of behavioral specification languages for modeling systems, in each case with a concern for the challenges of multicore programming. Furthermore, several of these efforts have attempted to provide data-race-free programming models, so that multicore programmers need not be faced with the added burden of trying to debug race conditions on top of the existing challenges of building reliable systems.

The dynamic nature of the medical domain is driving a need for continuous innovation and improvement in techniques for developing and assuring medical devices. Un-fortunately, research in academia and communication between academics, industrial engineers, and regulatory authorities is hampered by the lack of realistic non-proprietary development artifacts for medical devices. In this paper, we give an overview of a detailed requirements document for a Patient-Controlled Analgesic (PCA) pump developed under the US NSF's Food and Drug Administration (FDA) Scholar-in-Residence (SIR) program. This 60+ page document follows the methodology outlined in the US Federal Aviation Administrations (FAA) Requirements Engineering Management Handbook (REMH) and includes a domain overview, use cases, statements of safety & security requirements, and formal top-level system architectural description. Based on previous experience with release of a requirements document for a cardiac pacemaker that spawned a number of research and pedagogical activities, we believe that the described PCA requirements document can be an important research enabler within the formal methods and software engineering communities.

Recent experience in the avionics sector has demonstrated the benefits of using rigorous system architectural models, such as those supported by the standard Architectural and Analysis Definition Language (AADL), to ensure that multi-organization composition and integration tasks are successful. Despite its ability to capture interface signatures and system properties, such as scheduling periods and communication latencies as model attributes, AADL lacks a formal interface specification language, a formal semantics for component behavioral descriptions, and tools for reasoning about the compliance of behaviors to interface contracts. In this paper we introduce the Behavioral Language for Embedded Systems with Software (BLESS)—a behavioral interface specification language and proof environment for AADL. BLESS enables engineers to specify contracts on AADL components that capture both functional and timing properties. BLESS provides a formal semantics for AADL behavioral descriptions and automatic generation of verification conditions that, when proven by the BLESS proof tool, establish that behavioral descriptions conform to AADL contracts. We report on the application of BLESS to a collection of embedded system examples, including definition of multiple modes of a pacemaker.

Developing and certifying safety-critical and highly reliable systems almost always includes significant emphasis on hazard analysis and risk assessment. There have been substantial improvements in automation and formalization of other aspects of critical system engineering including model-driven development, analysis of source code and models, and verification techniques. However, hazard analysis and risk assessment are still largely manual and informal activities, tool support is limited (which for both development and auditing, increases time and effort and reduces accuracy and correctness), and artifacts are not integrated with architectural descriptions, system interfaces, high-level behavioral descriptions or code. The Error Model annex of the Architecture Analysis and Design Language (AADL) provides formal and automated support for a variety of forms of hazard analysis and risk assessment activities. Specifically, it enables engineers to formally specify errors, error propagation, error mitigation -- using annotations that are integrated with formal architecture and behavioral descriptions written in AADL. Plug-ins to the Open-Source AADL Tool Environment (OSATE) process these annotations to provide various forms of (semi)-automated support for reliability predication and tasks necessary to support common hazard analysis and risk assessment techniques such as Failure Modes and Effects Analysis (FMEA), Fault Tree Analysis (FTA), and Functional Hazard Analysis (FHA). In this paper, we illustrate basic aspects of Error Modeling in AADL using a simple safety-critical medical system -- an infant incubator called "Isolette". We summarize standard tasks involved in FMEA and FTA, we illustrate the principal steps involved in AADL Error Modeling for the Isolette, and we describe how those steps relate to FMEA and FTA. We give a brief survey of emerging automated analysis tools implemented as plug-ins to the AADL OSATE environment that process error modeling annotations. We believe this introduction to Error Modeling in AADL can expose engineers of high-integrity systems to techniques and tools that can provide a more rigorous, automated, and integrated approach to important risk management activities.

Existing regulatory agency guidance documents and process standards for medical devices (i.e., IEC 62304) generally consider medical devices to be stand-alone monolithic systems. The format and content of a system requirements document largely follows that of conventional embedded safety-critical systems. However, a vision is emerging of a new paradigm of medical system based on the notion of a medical application platform (MAP). A MAP is a safety- and security-critical real-time computing platform for (a) integrating heterogeneous devices, medical IT systems, and information displays via a communication infrastructure and (b) hosting application programs (i.e., apps) that provide medical utility via the ability to both acquire information from and update/control integrated devices, IT systems, and displays. To ensure a regulatory pathway for MAPs, it is necessary to adapt traditional development processes and artifacts to the specific characteristics of MAP architectures and constituent components. In this paper, we provide an initial proposal for developing and formatting requirements for MAP apps. For illustration, we consider an app that implements two “smart alarms” for pulse oximetry monitoring in a clinical context.