Logo des Repositoriums

Auflistung nach Schlagwort "Formal Verification"

1 - 6 von 6
  • Konferenzbeitrag
    Accountable Banking Transactions
    (Open Identity Summit 2024, 2024) Mödersheim, Sebastian; Chen, Siyu
    This paper shows how to apply the idea of Three branches of Accountability by Mödersheim and Cuellar to make banking transactions accountable, i.e., neither can the customer later deny to have placed the order, nor can the bank execute a transaction that the customer did not order. This is done in a general way that deliberately gives freedom to instantiate the system in several different ways, as long as it follows a few basic principles, and we show accountability holds in every instance.
  • Konferenzbeitrag
    Enhancing System-model Quality: Evaluation of the MontiBelle Approach with the Avionics Case Study on a Data Link Uplink Feed System
    (SE 2024 - Companion, 2024) Kausch, Hendrik; Pfeiffer, Mathias; Raco, Deni; Rumpe, Bernhard; Schweiger, Andreas
    Software quality is often related directly to the quality of the models used throughout the development phases. Assuring model quality can thus be an important aspect for assuring the quality of the final product. Measuring model quality is done via different quality indicators. In this article, we investigate the influence of our holistic systems engineering methodology on model quality. An avionics case study was previously conducted using our methodology. The developed SysML v2 model artifacts are evaluated in this paper regarding internal and external model quality, as well as model notation quality. In total, the positive impact on 26 model quality indicators from our previous work is argued. These indicators are divided into intra-model (single artifact) quality indicators and inter-model (across model artifact) quality indicators. The inter-model quality indicators are further classified into indicators for models at the same granularity level (horizontal) and across several granularity levels (vertical). Multiple quality indicators are positively affected by the modeling language’s capabilities and the underlying mathematical semantics. Other indicators depend on methodological guidelines that steer the engineering process. The evaluation of model-quality properties leads towards maturing a holistic systems engineering methodology that facilitates high model quality and thus indicates high product quality.
  • Konferenzbeitrag
    Formal Verification of Intelligent Hybrid Systems that are modeled with Simulink and the Reinforcement Learning Toolbox
    (Software Engineering 2023, 2023) Adelt, Julius; Liebrenz, Timm; Herber, Paula
    Reinforcement Learning (RL) is a powerful technique to control intelligent hybrid systems (HS) in dynamic and uncertain environments. However, formally guaranteeing safe behavior of intelligent HS is hard because formal descriptions are often not available in industrial design processes and hard to obtain for RL. Furthermore, the intertwined discrete and continuous behavior of hybrid systems results in limited scalability of automatic verification methods, such as model checking. This makes deductive verification desirable. In this paper, we summarize our approach for deductive verification of intelligent HS with embedded RL components that are modeled with Simulink and the RL Toolbox. This paper was originally published at the Formal Methods conference 2021 (FM21) [ALH21].
  • Zeitschriftenartikel
    From transistor level to cyber physical/hybrid systems: Formal verification using automatic compositional abstraction
    (it - Information Technology: Vol. 62, No. 5-6, 2020) Tarraf, Ahmad; Hedrich, Lars
    In this paper we present a methodology to automatically generate an accurate behavioral model from an analog circuit description. The current machine learning method is limited to circuits with up to 80 transistors, limiting our approach to small and mid size circuit blocks due to a state explosion problem. However, if complex building blocks such as IOT systems should be modeled, the current approach needs to recoup with feasible simulation and modeling time. To come up with a solution for this problem, we extend the current method by a compositional approach. The approach is illustrated upon an example from the area of autonomous driving. Our method decomposes this large example into smaller building blocks and models each of them automatically. All models are combined into a compositional hybrid automaton of the whole complex system. Compared to the original state space, the building blocks operate on smaller and reduced state spaces and hence drastically reduce the complexity. Using a back-transformation on the compositional automaton, all values from the original state space can be reconstructed. Moreover, we perform a formal verification on the generated compositional automaton. Results from a meaningful example are presented and discussed.
  • Konferenzbeitrag
    Modeling and Verification of Evolving Cyber-Physical Spaces
    (Software Engineering und Software Management 2018, 2018) Tsigkanos, Christos; Kehrer, Timo; Ghezzi, Carlo
    In this work, we report about recent research results on the Modeling and Verification of Evolving Cyber-Physical Spaces, published in ESEC/FSE17. We increasingly live in cyber-physical spaces – spaces that are both physical and digital, and where the two aspects are intertwined. Such spaces are highly dynamic and typically undergo continuous change. Software engineering can have a profound impact in this domain, by defining suitable modeling and specification notations as well as supporting design-time formal verification. In this paper, we present a methodology and a technical framework which support modeling of evolving cyber-physical spaces and reasoning about their spatio-temporal properties. We utilize a discrete, graph-based formalism for modeling cyber-physical spaces as well as primitives of change, giving rise to a reactive system consisting of rewriting rules with both local and global application conditions. Formal reasoning facilities are implemented adopting logic-based specification of properties and according model checking procedures, in both spatial and temporal fragments. We evaluate our approach using a case study of a disaster scenario in a smart city.
  • Konferenzbeitrag
    Verification of Plastic Interactive Systems
    (i-com: Vol. 14, No. 3, 2015) Oliveira, Raquel; Dupuy-Chessa, Sophie; Calvary, Gaëlle
    Interactive systems have largely evolved over the past years. Nowadays, different users can interact with systems on different devices and in different environments. The user interfaces (UIs) are expected to cope with such variety. Plastic UIs have the capacity to adapt to changes in their context of use while preserving usability. Such capability enhances UIs, however, it adds complexity on them. We propose an approach to verifying interactive systems considering this adaptation capability of the UIs. The approach applies two formal techniques: model checking, to the verification of properties over the system model, and equivalence checking, to compare different versions of a UI, thereby identifying different levels of UI equivalence. We apply the approach to a case study in the nuclear power plant domain in which several UI are analyzed, properties are verified, and the level of equivalence between them is demonstrated.