Abstract MDE enables the centrality of the models in semi-automated development processes. However, its level of usage in industrial settings is still not adequate for the benefits MDE can introduce. This paper proposes a semi-automatic approach for the completion of high-level models in the lifecycle of critical systems, which exhibit an event-driven behaviour. The proposal suggests a specification guideline that starts from a partial SysML model of a system and on a set of requirements, expressed in the well-known Given–When–Then paradigm. On the basis of such requirements, the approach enables the semi-automatic generation of new SysML state machines model elements. Accordingly, the approach focuses on the completion of the state machines by adding proper transitions (with triggers, guards and effects) among pre-existing states. Also, traceability modelling elements are added to the model. Two case studies demonstrate the feasibility of the proposed approach.

Even if the verification of authentication protocols can be achieved through formal analysis, the modelling of such an activity is an error-prone task due to the lack of automated and integrated processes. This paper relies on Unified Modeling Language (UML) profiling and model-transformation techniques to enable automatic analysis of authentication protocols starting from high-level models. The original contribution of this paper is a concrete toolchain, based on a modular approach, to support the modelling and analysis of authentication protocols. In particular, we propose three nested Extended Backus-Naur Form (EBNF) grammars for the high-level specification of the protocol and a transformation from the high-level specification into a specific target language, that is Alice & Bob extended (AnBx). The generated AnBx model can be then formally checked with the Open-Source Fixed-Point Model Checker (OFMC) tool. The validity and necessity of the proposed toolchain is demonstrated with a case study taken from the literature.

Abstract In recent years, we have seen many performance fiascos in the deployment of new systems, such as the US health insurance web. This paper describes the functionality and architecture, as well as success stories, of a tool that helps address these types of issues. The tool allows assessing software designs regarding quality, in particular performance and reliability. Starting from a UML design with quality annotations, the tool applies model-transformation techniques to yield analyzable models. Such models are then leveraged by the tool to compute quality metrics. Finally, quality results, over the design, are presented to the engineer, in terms of the problem domain. Hence, the tool is an asset for the software engineer to evaluate system quality through software designs. While leveraging the Eclipse platform, the tool uses UML and the MARTE, DAM and DICE profiles for the system design and the quality modeling.

Distributed Ledger Technology is demonstrating its capability to provide flexible frameworks for information assurance capable of resisting to byzantine failures and multiple target attacks. The availability of development frameworks allows the definition of many applications using such a technology. On the contrary, the verification of such applications are far from being easy since testing is not enough to guarantee the absence of security problems. The paper describes an experience in the modelling and security analysis of one of these applications by means of formal methods: in particular, we consider the Tweetchain protocol as a case study and we use the Tamarin Prover tool, which supports the modelling of a protocol as a multiset rewriting system and its analysis with respect to temporal first-order properties. With the aim of making the modeling and verification process reproducible and independent of the specific protocol, we present a general structure of the Tamarin Prover model and of the properties to verified. Finally, we discuss the strengths and limitations of the Tamarin Prover approach considering three aspects: modelling, analysis and the verification process. Copyright

Availability of a common, shared benchmark to provide repeatable, quantifiable, and comparable results is an added value for any scientific community. International consortia provide benchmarks in a wide range of domains, being normally used by industry, vendors, and researchers for evaluating their software products. In this regard, a benchmark of untimed Petri net models was developed to be used in a yearly software competition driven by the Petri net community. However, to the best of our knowledge there is not a similar benchmark to evaluate solution techniques for Petri nets with timing extensions. In this paper, we propose an evaluation framework for the comparative analysis of generalized stochastic Petri nets (GSPNs) simulation techniques. Although we focus on simulation techniques, our framework provides a baseline for a comparative analysis of different GSPN solvers (e.g., simulators, numerical solvers, or other techniques). The evaluation framework encompasses a set of 50 GSPN models including test cases and case studies from the literature, and a set of evaluation guidelines for the comparative analysis. In order to show the applicability of the proposed framework, we carry out a comparative analysis of steady-state simulators implemented in three academic software tools, namely, GreatSPN, PeabraiN, and TimeNET. The results allow us to validate the trustfulness of these academic software tools, as well as to point out potential problems and algorithmic optimization opportunities.

Model-driven techniques can be used to automatically produce formal models from different views of a system realised by using several modelling languages and notations. Specifications are transformed into formal models so facilitating the analysis of complex system for design, validation or verification purposes. However, no single formalism suits for representing all system’s views. In particular, the assessment of non-functional properties often requires integrated modelling approaches. The ultimate goal of the research work described in this paper is to develop a comprehensive, theoretical and practical framework able to support the development and the integration of new or existing model-driven approaches for the automatic generation of multi-formalism models. This paper defines the core theoretical ideas on which the framework is based and demonstrates their concrete applicability to the development of a multi-formalism approach for performability assessment.

Critical infrastructures, usually designed to handle disruptions caused by human errors or random acts of nature, define assets whose normal operation must be guaranteed to maintain its essential services for human daily living. Malicious intended attacks to these targets need to be considered during system design. To face these situations, defence plans must be developed in advance. In this paper, we present a Unified Modelling Language profile, named SecAM, that enables the modelling and security specification for critical infrastructures during the early phases (requirements, design) of system development life cycle. SecAM enables security assessment, through survivability analysis, of different security solutions before system deployment. As a case study, we evaluate the survivability of the Saudi Arabia crude-oil network under two different attack scenarios. The stochastic analysis, carried out with Generalized Stochastic Petri nets, quantitatively estimates the minimization of attack damages on the crude-oil network.

This paper presents a modeling methodology for clinical guidelines used in hospitals. The clinical guidelines are assumed to be given in a graphical form in a structure obtained by combining few elements. It is shown how the clinical guidelines represented with this syntax can be automatically converted into a mathematical model represented as Petri nets. The main advantage of the new model is the inclusion of resources and patient flow in the same model which makes possible its use in analysis and verification of the guidelines. Moreover, if different clinical guidelines in a hospital or department in a hospital are considered, the models can be used for resource optimization and performance evaluation. The clinical guideline of hip fracture from the ”Lozano Blesa” University hospital in Zaragoza is taken as an example.

The time Petri net with firing frequency intervals (TPNF) is a modeling formalism used to specify system behavior under timing and frequency constraints. Efficient techniques exist to evaluate the performance of TPNF models based on the computation of bounds of performance metrics (e.g., transition throughput, place marking). In this paper, we propose a min-max problem to compute the cycle time of a transition under optimistic assumptions. That is, we are interested in computing the lower bound. We will demonstrate that such a problem is related to a maximization linear programming problem (LP-max) previously stated in the literature, to compute the throughput upper bound of the transition. The main advantage of the min-max problem compared to the LP-max is that, in addition to the optimal value, the optimal solutions provide useful feedback to the analyst on the system behavior (e.g., performance bottlenecks). We have implemented two solution algorithms, using CPLEX APIs, to solve the min-max problem, and have compared their performance using a benchmark of TPNF models, several of these being case studies. Finally, we have applied the min-max technique for the vulnerability analysis of a critical infrastructure, i.e., the Saudi Arabian crude-oil distribution network.

Software systems that do not meet their timing constraints can cause risks. In this work, we propose a comprehensive method for assessing the risk of timing failure by evaluating the software design. We show how to apply best practises in software engineering and well-known Time Petri Net (TPN) modeling and analysis techniques, and we demonstrate the effectiveness of the method with reference to a case study in the domain of real-time embedded systems. The method customizes the Australian standard risk management process, where the system context is the UML-based software specification, enriched with standard MARTE profile annotations to capture nonfunctional system properties. During the risk analysis, a TPN is derived, via model transformation, from the software design specification and TPN bound techniques are applied to estimate the probability of timing failure. TPN bound techniques are also exploited, within the risk evaluation and treatment steps, to identify the risk causes in the software design.

Time Petri nets (TPNs) have been widely used for the verification and validation of real-time systems during the software development process. Their quantitative analysis consists in applying enumerative techniques that suffer the well known state space explosion problem. To overcome this problem, several methods have been proposed in the literature, that either provide rules to obtain equivalent nets with a reduced state space or avoid the construction of the whole state space. In this paper, we propose a method that consists in computing performance bounds to predict the average operational behavior of TPNs by exploiting their structural properties and by applying operational laws. Performance bound computation was first proposed for timed (Timed PNs) and stochastic Petri nets (SPNs). We generalize the results obtained for Timed PNs and SPNs to make the technique applicable to TPNs and their extended stochastic versions: TPN with firing frequency intervals (TPNFs) and extended TPNs (XTPNs). Finally, we apply the proposed bounding techniques on the case study of a robot-control application taken from the literature.

Reuse is a well-known and widely accepted principle in design and programming, that is instantiated through two main means: modularity and inheritance. Modularity allows a function or a data type and associated functions to be reused, while inheritance is based on the idea that a set of common features of a type can be factorized into a common supertype. While modularity has been widely exploited in performance and dependability modelling, inheritance is instead pretty much a "still-to-investigate" topic for this field. We discuss the role of inheritance in stochastic Petri nets (SPN) modelling, by considering a representation of the fault, error, and failure (FEF) chain based on hierarchies of classes (in the class diagram formalism of UML) and corresponding hierarchies of SPN models.

This paper presents a case study on the combined use of different tools and techniques for the validation and evaluation, from, the early stages of the design, of a fault tolerant software mechanism named distributed synchronization. The mechanism has been specified using UML state charts and sequence diagrams. A number of stochastic well-formed nets (SWN) models have been derived from the specifications: they have been composed using the tool algebra, and the resulting model has been model-checked using the PROD tool for temporal logic properties, thanks to a GreatSPN-to-PROD translator. The quantitative analysis has been performed using the SWN solvers of the Great-SPN tool.

Discusses the lessons learned in the modeling of a software fault tolerance solution built by a consortium of universities and industrial companies for an Esprit project called TIRAN (TaIlorable fault-toleRANce framework for embedded applications). The requirements of high flexibility and modularity for the software have lead to a modeling approach that is strongly based on compositionality. Since the interest was in assessing both the correctness and the performance of the proposed solution, we have cared for these two aspects at the same time, and, by means of an example, we show how this was a central aspect of our analysis.