Logo des Repositoriums

Auflistung nach Schlagwort "formal verification"

1 - 2 von 2
  • Zeitschriftenartikel
    Geordnete binäre Entscheidungsgraphen und ihre Bedeutung im rechnergestützten Entwurf hochintegrierter Schaltkreise
    (Informatik-Spektrum: Vol. 20, No. 5, 1997) Meinel, Christoph; Theobald, Thorsten
  • Konferenzbeitrag
    A Theory for Event-Driven Specifications Using Focus and MontiArc on the Example of a Data Link Uplink Feed System
    (Software Engineering 2023 Workshops, 2023) Kausch, Hendrik; Pfeiffer, Mathias; Raco, Deni; Rath, Amelie; Rumpe, Bernhard; Schweiger, Andreas
    The development of avionics message communication systems is expensive due to their complexity and the need to get them accepted by the certification authorities. We need to develop high-integrity software, but we also face cost pressure. For managing complex large systems, several time-synchronous modeling languages have been proposed. While these are appropriate for hardware specifications, when it comes to specifying distributed software systems, an event-based specification style is better suited. We present an event-based specification theory based on the framework Focus by giving the signatures and data types for specifications using event automata. For this, we capture message processing order as a further dimension of non-determinism by specifying a general timed merge component. These event automata can represent underspecification of behavior, and a refinement calculus can be applied to these for a stepwise reduction of non-determinism. Furthermore, we present the necessary concepts for enabling a user-friendly specification and simulation of event-based systems by using the architecture description language MontiArc. Finally, we evaluate our approach by performing a top-down architecture design of an avionics case study and demonstrating event-based specifications of requirements in MontiArc. The presented methodology improves the management of complexity, reduces costs, and increases the system quality.