In model-based systems engineering, system architectures often have to make compromises to meet hard constraints of functional and extra-functional requirements while optimizing for a target objective. Design space exploration (DSE) techniques have been developed to automatically propose candidate architectures over an extremely large design and configuration space. (1) Meta-heuristic exploration algorithms are often used to provide practical, best-effort solutions for DSE, but they lack any guarantees of completeness or optimality. (2) Logic synthesis based approaches may offer strong theoretical guarantees, but frequently face scalability issues. In the paper, we propose two logic solver-based approaches to evaluate complex design spaces by using partial models in order to find an optimal solution with respect to performability objectives. One approach uses performability analysis as a post-filtering of valid system architecture candidates, while the other approach uses performability analysis for guiding the actual search over partial models. We evaluate both approaches on an interferometry mission architecture case study using view transformations for performability analysis and compare our approach with a well-known DSE framework based on meta-heuristic search.

Abstract Algorithms and protocols with time dependent behavior are often specified formally using timed automata. For practical real-time systems, besides real-valued clock variables, these specifications typically contain discrete data variables with nontrivial data flow. In this paper, we propose a configurable lazy abstraction framework for the location reachability problem of timed automata that potentially contain discrete variables. Moreover, based on our previous work, we uniformly formalize in our framework several abstraction refinement strategies for both clock and discrete variables that can be freely combined, resulting in many distinct algorithm configurations. Besides the proposed refinement strategies, the configurability of the framework allows the integration of existing efficient lazy abstraction algorithms for clock variables based on $${\textit{LU}}$$ LU -bounds. We demonstrate the applicability of the framework and the proposed refinement strategies by an empirical evaluation on a wide range of timed automata models, including ones that contain discrete variables or diagonal constraints.

Abstract The increasing complexity of reactive systems can be mitigated with the use of components and composition languages in model-driven engineering. Designing composition languages is a challenge itself as both practical applicability (support for different composition approaches in various application domains), and precise formal semantics (support for verification and code generation) have to be taken into account. In our Gamma Statechart Composition Framework, we designed and implemented a composition language for the synchronous, cascade synchronous and asynchronous composition of statechart-based reactive components. We formalized the semantics of this composition language that provides the basis for generating composition-related Java source code as well as mapping the composite system to a back-end model checker for formal verification and model-based test case generation. In this paper, we present the composition language with its formal semantics, putting special emphasis on design decisions related to the language and their effects on verifiability and applicability. Furthermore, we demonstrate the design and verification functionality of the composition framework by presenting case studies from the cyber-physical system domain.

Since safety-critical autonomous vehicles need to interact with an immensely complex and continuously changing environment, their assurance is a major challenge. While systems engineering practice necessitates assurance on multiple levels, existing research focuses dominantly on component-level assurance while neglecting complex system-level traffic scenarios. In this paper, we aim to address the system-level testing of the situation-dependent behavior of autonomous vehicles by combining various model-based techniques on different levels of abstraction. (1) Safety properties are continuously monitored in challenging test scenarios (obtained in simulators or field tests) using graph query and complex event processing techniques. To precisely quantify the coverage of an existing test suite with respect regulations of safety standards, (2) we provide qualitative abstractions of causal, temporal, or geospatial data recorded in individual runs into situation graphs, which allows to systematically measure system-level situation coverage (on an abstract level) wrt. safety concepts captured by domain experts. Moreover, (3) we can systematically derive new challenging (abstract) situations which justifiably lead to runtime behavior which has not been tested so far by adapting consistent graph generation techniques, thus increasing situation coverage. Finally, (4) such abstract test cases are concretized so that they can be investigated in a real or simulated context.

In this paper, we present Theta, a configurable model checking framework. The goal of the framework is to support the design, execution and evaluation of abstraction refinement-based reachability analysis algorithms for models of different formalisms. It enables the definition of input formalisms, abstract domains, model interpreters, and strategies for abstraction and refinement. Currently it contains front-end support for transition systems, control flow automata and timed automata. The built-in abstract domains include predicates, explicit values, zones and their combinations, along with various refinement strategies implemented for each. The configurability of the framework allows the integration of several abstraction and refinement methods, this way supporting the evaluation of their advantages and shortcomings. We demonstrate the applicability of the framework by use cases for the safety checking of PLC, hardware, C programs and timed automata models.

Stochastic Petri nets are widely used for the modeling and analysis of non-functional properties of critical systems. The state space explosion problem often inhibits the numerical analysis of such models. Symbolic techniques exist to explore the discrete behavior of even complex models, while block Kronecker decomposition provides memory-efficient representation of the stochastic behavior. However, the combination of these techniques into a stochastic analysis approach is not straightforward. In this paper we integrate saturation-based symbolic techniques and decomposition-based stochastic analysis methods. Saturation-based exploration is used to build the state space representation and a new algorithm is introduced to efficiently build block Kronecker matrix representation to be used by the stochastic analysis algorithms. Measurements confirm that the presented combination of the two representations can expand the limits of previous approaches.

PetriDotNet is an extensible Petri net editor and analysis tool originally developed to support the education of formal methods. The ease of use and simple extensibility fostered more and more algorithmic developments. Thanks to the continuous interest of developers (especially M.Sc. and Ph.D. students who choose PetriDotNet as the framework of their thesis project), by now PetriDotNet became an analysis platform, providing various cutting-edge model checking algorithms and stochastic analysis algorithms. As a result, industrial application of the tool also emerged in recent years. In this paper we overview the main features and the architecture of PetriDotNet , and compare it with other available tools.

The complexity and quality needs of PLC-based control system software have largely increased. Formal specification methods can help to cope with these needs. Besides formal verification, another benefit of a formal specification language is the possibility to provide automatic generation of the final source code. This paper overviews PLCspecif, our formal specification language for PLC programs and presents a code generation method for the language. The result of the code generator is a Structured Text (ST) code that not only corresponds to the formal semantics of the specification, but is also configurable, readable, understandable, and follows development conventions and standards. The code generation method shows that PLC-specif is applicable and well-adapted to the PLC domain.

Abstract Efficient symbolic and explicit-state model checking approaches have been developed for the verification of linear time temporal logic (LTL) properties. Several attempts have been made to combine the advantages of the various algorithms. Model checking LTL properties usually poses two challenges: one must compute the synchronous product of the state space and the automaton model of the desired property, then look for counterexamples that is reduced to finding strongly connected components (SCCs) in the state space of the product. In case of concurrent systems, where the phenomenon of state space explosion often prevents the successful verification, the so-called saturation algorithm has proved its efficiency in state space exploration. This paper proposes a new approach that leverages the saturation algorithm both as an iteration strategy constructing the product directly, as well as in a new fixed-point computation algorithm to find strongly connected components on-the-fly by incrementally processing the components of the model. Complementing the search for SCCs, explicit techniques and component-wise abstractions are used to prove the absence of counterexamples. The resulting on-the-fly, incremental LTL model checking algorithm proved to scale well with the size of models, as the evaluation on models of the Model Checking Contest suggests.

Dealing with large, critical mobile systems and infrastructures where ongoing changes and resilience are paramount leads to very complex and difficult challenges for system evaluation. These challenges call for approaches that are able to integrate several evaluation methods for the quantitative assessment of QoS indicators which have been applied so far only to a limited extent. In this paper, we propose the holistic evaluation framework developed during the recently concluded FP6-HIDENETS project. It is based on abstraction and decomposition, and it exploits the interactions among different evaluation techniques including analytical, simulative, and experimental measurement approaches, to manage system complexity. The feasibility of the holistic approach for the analysis of a complete end-to-end scenario is first illustrated presenting two examples where mobility simulation is used in combination with stochastic analytical modeling, and then through the development and implementation of an evaluation workflow integrating several tools and model transformation steps.

Cost pressure, short time to market, and increased complexity are responsible for an evident increase of the failure rate of computing systems, while the cost of failures is growing rapidly, as a result of an unprecedented degree of dependence of our society on computing systems. The combination of these factors has created a dependability and security gap that is often perceived by users as a lack of trustworthiness in computer applications, and that is in fact undermining the network and service infrastructures that constitute the very core of the knowledge-based society.

This workshop summary gives a brief overview of the workshop on ldquoResilience Assessment and Dependability Benchmarkingrdquo held in conjunction with the 38th IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2008). The workshop aims at the presentation and exchange of ideas from the world wide research community and fostering discussions in order to give answers to the need for improving trustworthiness and understand the current risks inherent to computer systems and infrastructures. In particular the workshop aims at addressing key research challenges related to effective and accurate methods for measuring, assessing and benchmarking dependability and resilience.

This paper presents how the platform-specific development environment of time-triggered (TT) systems can be integrated with a visual design toolkit based on UML. The built-in facilities of UML and the modeling extensions introduced by us enable the unification of the advantages provided by both the embedded development environment and the UML tools. UML offers visual design, automatic code and documentation generation, while the underlying TT development environment offers platform-specific task and communication scheduling and fault tolerance middleware construction. This results in an integrated system that is capable of supporting the entire development within the framework of the UML tool

The VIATRA (visual automated model transformations) framework is the core of a transformation-based verification and validation environment for improving the quality of systems designed using the Unified Modeling Language by automatically checking consistency, completeness, and dependability requirements. In the current paper, we present an overview of (i) the major design goals and decisions, (ii) the underlying formal methodology based on metamodeling and graph transformation, (iii) the software architecture based upon the XMI standard, and (iv) several benchmark applications of the VIATRA framework.

The paper introduces a method which allows quantitative dependability analysis of systems modeled by using the Unified Modeling Language (UML) statechart diagrams. The analysis is performed by transforming the UML model to stochastic reward nets (SRNs). A large subset of statechart model elements is supported including event processing, state hierarchy and transition priorities. The transformation is presented by a set of SRN patterns. Performance-related measures can be directly derived using SRN tools, while dependability analysis requires explicit modeling of erroneous states and faulty behavior.

The paper deals with the automatic dependability analysis of systems designed using UML. An automatic transformation is defined for the generation of models to capture systems dependability attributes, like reliability. The transformation concentrates on structural UML views, available early in the design, to operate at different levels of refinement, and tries to capture only the information relevant for dependability to limit the size (state space) of the models. Due to the modular construction, these models can be refined later as more detailed, relevant information becomes available. Moreover a careful selection of those critical parts to be detailed allows one to avoid explosion of the size. An implementation of the transformation is in progress and will be integrated in the toolsets available for the ESPRIT LTR HIDE project.

Abstract. Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling Language (UML). In this paper we present a translation from a subset of UML Statechart Diagrams - covering essential aspects of both concurrent behaviour, like sequentialisation, parallelism, non-determinism and priority, and state refinement - into PROMELA, the specification language of the SPIN model checker. SPIN is one of the most advanced analysis and verification tools available nowadays. Our translation allows for the automatic verification of UML Statechart Diagrams. The translation is simple, proven correct, and promising in terms of state space representation efficiency.