The Experts below are selected from a list of 5118 Experts worldwide ranked by ideXlab platform
Istvan Majzik - One of the best experts on this subject based on the ideXlab platform.
-
the gamma statechart composition framework design verification and code generation for component based reactive systems
International Conference on Software Engineering, 2018Co-Authors: Vince Molnar, Istvan Majzik, Bence Graics, Andras Voros, Daniel VarroAbstract:The Gamma Statechart Composition Framework is an integrated tool to support the design, verification and validation as well as code generation for component-based reactive systems. The behavior of each component is captured by a statechart, while assembling the system from components is driven by a domain-specific composition language. Gamma automatically synthesizes executable Java code extending the output of existing statechart-based code generators with composition related parts, and it supports formal verification by mapping composite Statecharts to a back-end model checker. Execution traces obtained as witnesses during verification are back-annotated as test cases to replay an error trace or to validate external code generators. Tool demonstration video: https://youtu.be/ng7lKd1wlDo
-
exploiting hierarchy in the abstraction based verification of Statecharts using smt solvers
FESCA@ETAPS, 2017Co-Authors: Bence Czipo, Akos Hajdu, Tamas Toth, Istvan MajzikAbstract:Statecharts are frequently used as a modeling formalism in the design of state-based systems. Formal verification techniques are also often applied to prove certain properties about the behavior of the system. One of the most efficient techniques for formal verification is Counterexample-Guided Abstraction Refinement (CEGAR), which reduces the complexity of systems by automatically building and refining abstractions. In our paper we present a novel adaptation of the CEGAR approach to hierarchical statechart models. First we introduce an encoding of the statechart to logical formulas that preserves information about the state hierarchy. Based on this encoding we propose abstraction and refinement techniques that utilize the hierarchical structure of Statecharts and also handle variables in the model. The encoding allows us to use SMT solvers for the systematic exploration and verification of the abstract model, including also bounded model checking. We demonstrate the applicability and efficiency of our abstraction techniques with measurements on an industry-motivated example.
-
checking general safety criteria on uml Statecharts
International Conference on Computer Safety Reliability and Security, 2001Co-Authors: Zsigmond Pap, Istvan Majzik, Andras PatariczaAbstract:This paper describes methods and tools for automated safety analysis of UML statechart specifications. The general safety criteria described in the literature are reviewed and automated analysis techniques are proposed. The techniques based on OCL expressions and graph transformations are detailed and their limitations are discussed. To speed up the checker methods, a reduced form for UML Statecharts is introduced. Using this form, the correctness and completeness of some checker methods can be proven. An example illustrates the application of the tools developed so far.
-
towards a formal operational semantics of uml statechart diagrams
Formal Methods for Open Object-Based Distributed Systems, 1999Co-Authors: Diego Latella, Istvan Majzik, Mieke MassinkAbstract:Statechart Diagrams are a notation for describing behaviours in the framework of UML, the Unified Modeling Language of object-oriented systems. UML is a semi-formal language, with a precisely defined syntax and static semantics but with an only informally specified dynamic semantics. UML Statechart Diagrams differ from classical Statecharts, as defined by Harel, for which formalizations and results are available in the literature. This paper sets the basis for the development of a formal semantics for UML Statechart Diagrams based on Kripke structures. This forms the first step towards model checking of UML Statechart Diagrams. We follow the approach proposed by Mikk and others: we first map Statechart Diagrams to the intermediate format of extended hierarchical automata and then we define an operational semantics for these automata. We prove a number of properties of such semantics which reflect the design choices of UML Statechart Diagrams.
Lui Sha - One of the best experts on this subject based on the ideXlab platform.
-
formalism for supporting the development of verifiably safe medical guidelines with Statecharts
arXiv: Software Engineering, 2019Co-Authors: Chunhui Guo, Zhenyu Zhang, Shangping Ren, Lui ShaAbstract:Improving the effectiveness and safety of patient care is the ultimate objective for medical cyber-physical systems. Many medical best practice guidelines exist, but most of the existing guidelines in handbooks are difficult for medical staff to remember and apply clinically. Furthermore, although the guidelines have gone through clinical validations, validations by medical professionals alone do not provide guarantees for the safety of medical cyber-physical systems. Hence, formal verification is also needed. The paper presents the formal semantics for a framework that we developed to support the development of verifiably safe medical guidelines. The framework allows computer scientists to work together with medical professionals to transform medical best practice guidelines into executable statechart models, Yakindu in particular, so that medical functionalities and properties can be quickly prototyped and validated. Existing formal verification technologies, UPPAAL timed automata in particular, is integrated into the framework to provide formal verification capabilities to verify safety properties. However, some components used/built into the framework, such as the open-source Yakindu Statecharts as well as the transformation rules from Statecharts to timed automata, do not have built-in semantics. The ambiguity becomes unavoidable unless formal semantics is defined for the framework, which is what the paper is to present.
-
design verifiably correct model patterns to facilitate modeling medical best practice guidelines with Statecharts
IEEE Internet of Things Journal, 2019Co-Authors: Chunhui Guo, Zhenyu Zhang, Shangping Ren, Lui ShaAbstract: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 implementation’s 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.
Kadir Alpaslan Demir - One of the best experts on this subject based on the ideXlab platform.
-
creating and validating embedded assertion Statecharts
IEEE Distributed Systems Online, 2007Co-Authors: Doron Drusinsky, Mantak Shing, Kadir Alpaslan DemirAbstract:Integrating formal assertions into the modeling, implementation, and testing of statechart-based designs can enhance a rapid system prototyping system's robustness by providing runtime monitoring and recovery from assertion failures. An iterative process for developing and verifying statechart prototype models augmented with statechart assertions using the StateRover tool lets system designers write formal specifications using statechart assertions. It also enables them to use JUnit-based simulation to validate statechart assertions and to test statechart prototype models augmented with statechart assertions. A case study using a safety-critical computer assisted resuscitation algorithm software prototype for a casualty intravenous fluid infusion pump illustrates the process.
-
creation and validation of embedded assertion Statecharts
Rapid System Prototyping, 2006Co-Authors: Doron Drusinsky, Mantak Shing, Kadir Alpaslan DemirAbstract:This paper addresses the need to integrate formal assertions into the modeling, implementation, and testing of statechart based designs. The paper describes an iterative process for the development and verification of statechart prototype models augmented with statechart assertions using the StateRover tool. The novel aspects of the proposed process include (1) writing formal specifications using statechart assertions, (2) JUnit-based simulation and validation of statechart assertions, (3) JUnit-based simulation and testing of statechart prototype models augmented with statechart assertions, (4) automatic, JUnit-based, white-box testing of statechart prototypes augmented with statechart assertions, and (5) spiral adjustment of model and specification using the test results. We demonstrate the proposed process with a prototype of a safety-critical computer assisted resuscitation algorithm (CARA) software for a casualty intravenous fluid infusion pump
Harbhajan Singh - One of the best experts on this subject based on the ideXlab platform.
-
testing a system specified using Statecharts and z
Information & Software Technology, 2001Co-Authors: Robert M Hierons, Sadegh Sadeghipour, Harbhajan SinghAbstract:Abstract A hybrid specification language μSZ, in which the dynamic behaviour of a system is described using Statecharts and the data and the data transformations are described using Z, has been developed for the specification of embedded systems. This paper describes an approach to testing from a deterministic sequential specification written in μSZ. By considering the Z specifications of the operations, the extended finite state machine (EFSM) defined by the Statechart can be rewritten to produce an EFSM that has a number of properties that simplify test generation. Test generation algorithms are introduced and applied to an example. While this paper considers μSZ specifications, the approaches described might be applied whenever the specification is an EFSM whose states and transitions are specified using a language similar to Z.
Michael Von Der Beeck - One of the best experts on this subject based on the ideXlab platform.
-
a structured operational semantics for uml Statecharts
Software and Systems Modeling, 2002Co-Authors: Michael Von Der BeeckAbstract:The Unified Modeling Language (UML) has gained wide acceptance in very short time because of its variety of well-known and intuitive graphical notations. However, this comes at the price of an unprecise and incomplete semantics definition. This insufficiency concerns single UML diagram notations on their own as well as their integration. In this paper, we focus on the notation of UML-Statecharts. Starting with a precise textual syntax definition, we develop a precise structured operational semantics (SOS) for UML-Statecharts. Besides the support of interlevel transitions and in contrast to related work, our semantics definition supports characteristic UML-statechart features like the history mechanism as well as entry and exit actions.
-
formalization of uml Statecharts
Lecture Notes in Computer Science, 2001Co-Authors: Michael Von Der BeeckAbstract:The Unified Modeling Language (UML) has gained wide acceptance in very short time because of its variety of well-known and intuitive graphical notations. However, this comes at the prize of an unprecise and incomplete semantics definition. This insufficiency concerns single UML diagram notations on their own as well as their integration. In this paper, we focus on the notation of UML-Statecharts. Starting with a precise textual syntax definition, we develop quite a concise structured operational semantics (SOS) for UML-Statecharts based on labeled transition systems. Besides the support of interlevel transitions and in contrast to related work, our semantics definition supports characteristic UML-Statechart features like the history mechanism as well as entry and exit actions.
-
a compositional approach to Statecharts semantics
Foundations of Software Engineering, 2000Co-Authors: Gerald Luttgen, Michael Von Der Beeck, Rance CleavelandAbstract:Statecharts is a visual language for specifying reactive system behavior. The formalism extends traditional finite-state machines with notions of hierarchy and concurrency, and it is used in many popular software design notations. A large part of the appeal of Statecharts derives from its basis in state machines, with their intuitive operational interpretation. The classical semantics of Statecharts, however, suffers from a serious defect; it is not compositional, meaning that the behavior of system descriptions cannot be inferred from the behavior of their subsystems. Compositionality is a prerequisite for exploiting the modular structure of Statecharts for simulation, verification, and code generation, and it also provides the necessary foundation for reusability.This paper suggests a new compositional approach to formalizing Statecharts semantics as flattened labeled transition systems in which transitions represent system steps. The approach builds on ideas developed for timed process calculi and employs structural operational rules to define the transitions of a Statecharts expression in terms of the transitions of its subexpressions. It is first presented for a simple dialect of Statecharts, with respect to a variant of Pnueli and Shalev's semantics, and is illustrated by means of a small example. To demonstrate its flexibility, the proposed approach is then extended to deal with practically useful features available in many Statecharts variants, namely state references, history states, and priority concepts along state hierarchies.
-
a comparison of Statecharts variants
International Symposium Organized Jointly with Working Group Provably Correct Systems on Formal Techniques in Real-Time and Fault-Tolerant Systems, 1994Co-Authors: Michael Von Der BeeckAbstract:The Statecharts formalism supports the development of intuitive graphical specifications for reactive systems. Nevertheless, some serious problems became apparent in the original Statecharts formalism so that many different Statecharts variants were proposed to overcome them. These problems are thoroughly described and approaches for solving them are evaluated. Furthermore, a set of distinctive features is elaborated which is used for a detailed comparison of the Statecharts variants. Finally, the feature set is used to characterize a new hypothetical Statecharts variant.
