Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userDesignBIP: A Design Studio for Modeling and Generating Systems with BIP
96
0
0.0
(
0
)
Added by
EPTCS
Publication date
2018
fields
Informatics Engineering
and research's language is
English
Authors
Anastasia Mavridou
Ask ChatGPT about the research
No Arabic abstract
The Behavior-Interaction-Priority (BIP) framework, rooted in rigorous semantics, allows the construction of systems that are correct-by-design. BIP has been effectively used for the construction and analysis of large systems such as robot controllers and satellite on-board software. Nevertheless, the specification of BIP models is done in a purely textual manner without any code editor support. To facilitate the specification of BIP models, we present DesignBIP, a web-based, collaborative, version-controlled design studio. To promote model scaling and reusability of BIP models, we use a graphical language for modeling parameterized BIP models with rigorous semantics. We present the various services provided by the design studio, including model editors, code editors, consistency checking mechanisms, code generators, and integration with the JavaBIP tool-set.
rate research
Read More
Improving patient care safety is an ultimate objective for medical cyber-physical systems. A recent study shows that the patients death rate can be significantly reduced by computerizing medical best practice guidelines. To facilitate the development of computerized medical best practice guidelines, statecharts are often used as a modeling tool because of their high resemblances to disease and treatment models and their capabilities to provide rapid prototyping and simulation for clinical validations. However, some implementations of statecharts, such as Yakindu statecharts, are priority-based and have synchronous execution semantics which makes it difficult to model certain functionalities that are essential in modeling medical guidelines, such as two-way communications and configurable execution orders. Rather than introducing new statechart elements or changing the statechart implementations underline semantics, we use existing basic statechart elements to design model patterns for the commonly occurring issues. In particular, we show the design of model patterns for two-way communications and configurable execution orders and formally prove the correctness of these model patterns. We further use a simplified airway laser surgery scenario as a case study to demonstrate how the developed model patterns address the two-way communication and configurable execution order issues and their impact on validation and verification of medical safety properties.
Improving patient care safety is an ultimate objective for medical cyber-physical systems. A recent study shows that the patients death rate is significantly reduced by computerizing medical best practice guidelines. Recent data also show that some morbidity and mortality in emergency care are directly caused by delayed or interrupted treatment due to lack of medical resources. However, medical guidelines usually do not provide guidance on medical resource demands and how to manage potential unexpected delays in resource availability. If medical resources are temporarily unavailable, safety properties in existing executable medical guideline models may fail which may cause increased risk to patients under care. The paper presents a separately model and jointly verify (SMJV) architecture to separately model medical resource available times and relationships and jointly verify safety properties of existing medical best practice guideline models with resource models being integrated in. The SMJV architecture allows medical staff to effectively manage medical resource demands and unexpected resource availability delays during emergency care. The separated modeling approach also allows different domain professionals to make independent model modifications, facilitates the management of frequent resource availability changes, and enables resource statechart reuse in multiple medical guideline models. A simplified stroke scenario is used as a case study to investigate the effectiveness and validity of the SMJV architecture. The case study indicates that the SMJV architecture is able to identify unsafe properties caused by unexpected resource delays.
Improving effectiveness and safety of patient care is an ultimate objective for medical cyber-physical systems. A recent study shows that the patients death rate can be reduced by computerizing medical guidelines. Most existing medical guideline models are validated and/or verified based on the assumption that all necessary medical resources needed for a patient care are always available. However, the reality is that some medical resources, such as special medical equipment or medical specialists, can be temporarily unavailable for an individual patient. In such cases, safety properties validated and/or verified in existing medical guideline models without considering medical resource availability may not hold any more. The paper argues that considering medical resource availability is essential in building verifiably correct executable medical guidelines. We present an approach to explicitly and separately model medical resource availability and automatically integrate resource availability models into an existing statechart-based computerized medical guideline model. This approach requires minimal change in existing medical guideline models to take into consideration of medical resource availability in validating and verifying medical guideline models. A simplified stroke scenario is used as a case study to investigate the effectiveness and validity of our approach.
Existing model-based processes for embedded real-time systems support the analysis of various non-functional properties, most notably schedulability, through model checking, simulation or other means. The analysis results are then used for modifying the systems design, so that the expected properties are satisfied. A rigorous model-based design flow differs in that it aims at a system implementation derived from high-level models by applying a sequence of semantics-preserving transformations. Properties established at any design step are preserved throughout the subsequent steps including the executable implementation. We introduce such a design flow using a process network model of computation for application design at a high level, which combines streaming and reactive control processing with task parallelism. The schedulability of the so-called FPPNs (Fixed Priority Process Networks) is well-studied and various solutions have been presented. This article focuses on the design flows steps for deriving executable implementations on the BIP (Behavior - Interaction - Priority) runtime environment. FPPNs are designed using the TASTE toolset, a convenient architecture description interface. In this way, the developers do not program explicitly low-level real-time OS services and the schedulability properties are guaranteed throughout the design steps by construction. The approach has been validated on the design of a real spacecraft on-board application that has been scheduled for execution on an industrial multicore platform.
Cyber-physical systems combine software and physical components. Specification-driven trace-checking tools for CPS usually provide users with a specification language to express the requirements of interest, and an automatic procedure to check whether these requirements hold on the execution traces of a CPS. Although there exist several specification languages for CPS, they are often not sufficiently expressive to allow the specification of complex CPS properties related to the software and the physical components and their interactions. In this paper, we propose (i) the Hybrid Logic of Signals (HLS), a logic-based language that allows the specification of complex CPS requirements, and (ii) ThEodorE, an efficient SMT-based trace-checking procedure. This procedure reduces the problem of checking a CPS requirement over an execution trace, to checking the satisfiability of an SMT formula. We evaluated our contributions by using a representative industrial case study in the satellite domain. We assessed the expressiveness of HLS by considering 212 requirements of our case study. HLS could express all the 212 requirements. We also assessed the applicability of ThEodorE by running the trace-checking procedure for 747 trace-requirement combinations. ThEodorE was able to produce a verdict in 74.5% of the cases. Finally, we compared HLS and ThEodorE with other specification languages and trace-checking tools from the literature. Our results show that, from a practical standpoint, our approach offers a better trade-off between expressiveness and performance.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
