We present a Model Driven Engineering (MDE) approach to dependability evaluation of component-based coherent dyadic systems, implemented by the FaultFlow library, combining simple high-level modeling with powerful quantitative evaluation methods. In the functional perspective, distinctive features are: modeling of fault propagations within individual components and between different components, possibly not connected through physical or communication interfaces; support for non-Markovian distributions, both for the times to the occurrence of faults and for the duration of fault-to-failure propagations; derivation of the distribution of the time to the occurrence of a given failure; derivation of fault importance measures, for models where each fault does not propagate into multiple failures and, viceversa, each failure does not act as fault to multiple components, achieving evaluation efficiency even for significantly complex systems with hundreds of different faults. In the implementation perspective, distinctive features are: definition of a custom-made extensible metamodel to specify the system structure and failure logic; automated derivation of metamodel instances from Systems Modeling Language (SysML) Block Definition Diagrams (BDDs) and Stochastic Static Fault Trees (SSFTs); automated derivation of the mentioned dependability measures; open source availability. We illustrate the typical modeling and evaluation workflow with relevant uses cases, comparing functionalities with those of other dependability evaluation tools.

Technological advances in modern Train Control Systems (TCSs) promise to improve dependability of railway transportation in terms of safety, availability, and capacity, notably by employing novel distancing policies such as Moving Block (MB) signaling and Virtual Coupling (VC), fueled by advanced train localization methods such as satellite positioning. At the same time, these technological advances raise notable concerns about the effects that uncertainty in critical TCS parameters (such as train position and speed) may have on dependability-related attributes. Recently, various approaches have been proposed to characterize such effects through quantitative measures, leveraging formal stochastic modeling and evaluation of the TCS behavior. In this paper, we illustrate the results of a systematic review of the literature on quantitative evaluation of dependability-related attributes of TCSs under uncertainty on vital parameters. Specifically, we have finally selected 42 relevant papers, published between 2011 and 2023, that succeed in giving, through an empirical perspective and classification, a comprehensive view of current research and practice in quantitative dependability assessment of TCSs.

In performance engineering of composed services, coordinated provisioning can reduce the amount of resources required to meet end-to-end response time objectives. To this aim, various intertwined aspects of the application architecture need to be taken into account, notably including precedence constraints in the composition of elementary services, along with their durations and sensitivity to the scaling of provisioned resources. We address coordinated provisioning of resources for elementary services with stochastic durations with general distributions (i.e., including non-exponential distributions). We compose services in a workflow where precedence constraints define a Directed Acyclic Graph (DAG) and the distribution of the end-to-end (E2E) response time is subject to a Service Level Objective (SLO). We leverage a surrogate model of service performance, assuming a low workload of workflow requests (i.e., a single-request scenario) and service durations inversely proportional to provisioned resources. Given the total amount of resources, our approach derives the service provisioning that optimizes the workflow E2E response time distribution, by exploiting a compositional approach and by using stochastically ordered approximations to manage dependencies in non-well-nested precedence DAGs. Then, the approach scales provisioned resources up or down to determine the minimum amount of resources needed to satisfy the SLO, while leaving the remaining resources for horizontal scaling in order to manage multiple workflow requests at high workloads. Experiments consider low-workload and high-workload scenarios, different relations between elementary service durations and provisioned resources, and workflow topologies taken from benchmarks or randomly generated with controlled statistics, using elementary service durations from a dataset of the literature. Results show that the technique is feasible also for workflows with a thousand of services and that it outperforms other provisioning methods in fitting the SLO using the same resource amount and in minimizing the resource amount needed to fit the SLO.

Effective exploitation of Machine Learning solutions in the Digital Twin (DT) paradigm may largely benefit from Federated Analytics (FA) approaches, to mitigate data scarcity, by merging distributed data, and heterogeneity while limiting communication overhead and exchange of sensitive raw data. In the DT paradigm, federated schemes find a native collocation in the conceptual association between Digital Twin Prototype (DTP) of a class and Digital Twin Instance (DTI) of individual products. We propose the application of the democratized learning (Dem-AI) scheme to provide a scalable solution for multi-level hierarchical integration of data owned by a multiplicity of distributed DTs, and we showcase its application in a failure prediction scenario. The proposed model integration scheme preserves the inherent cohesive relationships between generalization and specialization (or personalization) capabilities of the DTP model and the DTI model, respectively. Based on the model acquired, DTs monitor the system behavior and forecast failure occurrences. Experimental analysis has been conducted to thoroughly investigate the performance of the Dem-AI failure prediction framework designed, considering different levels of model specialization and public dataset.

In component-based software systems, micro-rejuvenation of individual components can be performed to limit the number of more time-consuming system macro-rejuvenations, requiring appropriate selection of rejuvenation times to actually reduce the system unavailability. We present a novel coordinated approach to micro-rejuvenation of software components, aimed at minimizing the system cumulative unavailability over time.Specifically, each component is periodically rejuvenated, and, if it fails, rejuvenation is scheduled after repair. To limit concurrent component rejuvenations, an efficient calculus is defined to derive the optimal rejuvenation offset of each component, based on the condition of system unavailability expressed as a static fault tree with AND and OR gates. An efficient compositional approach is also provided to derive the system unavailability, by leveraging numerical analysis of a stochastic model with underlying Markov regenerative process. The solution accuracy is exploited to analyze how components loose synchronization over time due to random rejuvenation and repair times, enabling the definition of a macro-rejuvenation policy. Experiments performed on several randomly and manually generated models show feasibility and effectiveness of the approach, enabling further extensions.

Quantitative evaluation of stochastic models supports early verification of design choices and assessment of non-functional requirements. Model Driven Engineering (MDE) leverages automated derivation of formal stochastic models from semi-formal artifacts of the Unified Modeling Language (UML) to facilitate deployment of quantitative evaluation methods without disrupting industrial practices. As a major limitation, when generally distributed (GEN) temporal parameters are considered to enhance the model expressivity, the structure and complexity of the underlying stochastic process cannot be easily controlled, possibly impairing the model analyzability. We present a hierarchical modeling formalism based on UML statecharts with GEN durations, designed to guarantee ease of modeling and efficient evaluation of steady-state or transient behaviour until absorption. To this end, fairly lax restrictions are applied to the model syntax to enable separate analysis of the Semi-Markov Process (SMP) underlying each model component. Scalability of solution is assessed by analyzing a suite of synthetic models referred to the context of timed Failure Logic Analysis (FLA) of component-based systems, specifically designed to point out each factor of computational complexity. Notably, the analysis derives both the probability that the system is in each step before failure and the Cumulative Distribution Function (CDF) of the duration of the overall failure process. A challenging case study that significantly and jointly stresses the main factors of computational complexity is finally addressed, performing steady-state analysis of a non-Markovian variant of a server virtualized system from the literature on software rejuvenation.

Workflows are patterns of orchestrated activities designed to deliver some specific output, with application in various relevant contexts including software services, business processes, supply chain management. In most of these scenarios, durational properties of individual activities can be identified from logged data and cast in stochastic models, enabling quantitative evaluation of time behavior for diagnostic and predictive analytics. However, effective fitting of observed durations commonly requires that distributions break the limits of memoryless behavior and unbounded support of Exponential distributions, casting the problem in the class of non-Markovian models. This results in a major hurdle for numerical solution, largely exacerbated by the concurrency structure of workflows, which natively subtend concurrent activities with overlapping execution intervals and a limited number of regeneration points, i.e., time points at which the Markov property is satisfied and analysis can be decomposed according to a renewal argument. We propose a compositional method for quantitative evaluation of end-to-end response time of complex workflows. The workflow is modeled through Stochastic Time Petri Nets (STPNs), associating activity durations with Exponential distributions truncated over bilateral firmly bounded supports that fit mean and coefficient of variation of real logged histograms. Based on the model structure, the workflow is decomposed into a hierarchy of subworkflows, each amenable to efficient numerical solution through Markov regenerative transient analysis. In this step, the grain of decomposition is driven by non-deterministic analysis of the space of feasible behaviors in the underlying Time Petri Net (TPN) model, which permits efficient characterization of the factors that affect behavior complexity between regeneration points. Duration distributions of the subworkflows obtained through separate analyses are then repeatedly recomposed in numerical form to compute the response time distribution of the overall workflow.

In systems with imperfect fault coverage (IFC), all components are subject to uncovered failures, possibly threatening the whole system. Therefore, to improve the system reliability, it is important to timely detect, identify, and shut down the components that are no more relevant for the system operation. This article addresses quantitative evaluation of the relevance of components, assuming that they have independent and identically distributed lifetimes to characterize the impact of the system design only on the system reliability and energy consumption. To this end, the dynamic relevance measure is defined to characterize the irrelevant components in different stages of the system lifetime depending on the number of occurred component failures, supporting the evaluation of the probability that the system fails due to uncovered failures of irrelevant components. Moreover, the system reliability over time is also efficiently derived, both in the case that irrelevance is not considered and in the case that irrelevant components can be immediately isolated, notably supporting any general (i.e., non-Markovian) distribution for the failure time of components. Feasibility and effectiveness of the approach are assessed on two real-scale case studies addressing reliability evaluation of a flight control system and a multihop wireless sensor network.

We present the next generation of ORIS, a toolbox for quantitative evaluation of concurrent models with non-Markovian timers. The tool shifts its focus from timed models to stochastic ones, it includes a new graphical user interface, new analysis methods and a Java Application Programming Interface (API). Models can be specified as Stochastic Time Petri Nets (STPNs) through the graphical editor, validated using an interactive token game, and analyzed through several techniques to compute instantaneous or cumulative rewards. STPNs can also be exported as Java code to conduct extensive parametric studies through the Java library, now distributed as open-source. A well-engineered software architecture allows the user to implement new features for STPNs, new modeling formalisms, and new analysis methods. The most distinctive features of ORIS include transient and steady-state analysis of STPNs modeling Markov Regenerative Processes (MRPs), and transient analysis of STPNs modeling generalized semi-Markov processes. ORIS also supports state-space analysis of Time Petri Nets (TPNs), simulation of STPNs, and standard analysis techniques for continuous-time Markov chains or MRPs with at most one non-exponential timer in each state. We illustrate the general workflow for the application of ORIS to the modeling and evaluation of non-functional requirements of software-intensive systems.

A Water Distribution System (WDS) is a critical infrastructure for society and economy, subject to frequent maintenance either for contingencies or planned operations. Maintenance procedures affect the hybrid dynamics of a WDS at stochastic time points, representing the completion of repair activities that change the WDS topology and operation mode. Hence, the problem of performability evaluation of the WDS behavior during a maintenance intervention falls in the class of stochastic hybrid systems (SHSs), for which existing numerical or simulative approaches cannot afford the complexity of realistic WDSs. We propose a viable approach that computes the expected demand not served during a maintenance procedure by integrating fluid-dynamic analysis of the WDS with quantitative evaluation of the procedure timing, notably assuming non-Markovian repair times over a bounded support. Different solution techniques are presented to evaluate the joint distribution of the times when the procedure affects the WDS, performing either simulation of the procedure model or state-space analysis based on an extension of the method of stochastic state classes. Feasibility and effectiveness of the proposed methods are assessed on a real WDS in terms of result accuracy and computational complexity, showing that the overall approach could be efficiently applied in higher level tasks including activity scheduling, resource planning, and budget allocation.

Runtime predictive analysis of quantitative models can support software reliability in various application scenarios. The spread of logging technologies promotes approaches where such models are learned from observed events. We consider a system visiting transient states of a hidden process until reaching a final state and producing observations with stochastic arrival times and types conditioned by visited states, and we abstract it as a marked Markov modulated Poisson Process (MMMPP) with left-to right structure. We present an Expectation-Maximization (EM) algorithm that learns the MMMPP parameters from observation sequences acquired in repeated execution of the transient behavior, and we use the model at runtime to infer the current state of the process from actual observed events and to dynamically evaluate the remaining time to the final state. The approach is illustrated using synthetic datasets generated from a stochastic attack tree of the literature enriched with an observation model associating each state with an expected statistics of observation types and arrival times. Accuracy of prediction is evaluated under different variability of hidden states sojourn durations and of the observations arrival process, and compared against previous literature that mainly exploits either the timing or the types of observed events.

We propose an approach for assessing the impact of multi-phased repair procedures on gas distribution networks, capturing load profiles that can depend on time for different classes of users, suspension of activities during non-working hours, and random execution times depending on topological, physical, and geographical characteristics of the network. The problem is characterized through a semi-formal specification based on artifacts of the Systems Modeling Language (SysML), which is then translated into a formal model based on stochastic time Petri nets. The solution method interleaves fluid-dynamic analysis of the gas behavior and stochastic analysis of the time spent in the repair process, decoupling complexities and making stochastic analysis almost insensitive to the network size and topology. Hence, our approach turns out to be applicable to real scale cases, notably computing the optimal time of day to start the repair procedure. Moreover, by encompassing general (non-Markovian) distributions, the approach enables effective fitting of durations.

We present a model-based approach to Activity Recognition (AR) in Ambient Assisted Living (AAL). The approach leverages an a priori stochastic model termed Continuous-Time Hidden Semi-Markov Model (CT-HSMM), capturing the continuous-time durations of activities and inter-event times. The model is enhanced according to the observed statistics, associating the events with an occurrence probability, and the sojourn time and the inter-event time in each activity with a continuous-time probability density function, allowing effective fitting of observed durations through non-Markovian distributions. The model is updated at run time according to a sequence of time-stamped observations, exploiting the method of stochastic state classes to perform transient analysis and derive a measure of likelihood that an activity is currently performed. The approach supports both online AR, predicting the activity performed at time t using only the events observed until that time, and offline AR, applying a forward- backward procedure that exploits all the events observed before and after time t. The approach is experimented on a real dataset of the literature, providing performance measures that can be compared with those of offline Hidden Markov Models (HMMs) and offline Hidden Semi-Markov Models (HSMMs).

Agile production systems face major issues in satisfying fickle market needs in highly demand-driven industry sectors, such as electronics and mechatronics. In this context, the time needed to complete the production of an item tends to be highly variable, and online estimation of the remaining completion time may suffer the lack of adequate sensor data, especially in existing manufacturing systems. To solve this issue, we propose a new analytical technique for the evaluation of an upper and a lower stochastic bound on the remaining completion time of a product, considering an assembly line made of sequential workstations with transfer blocking and buffer capacity. The approach notably encompasses service times with non-Markovian distribution, and avoids the limitation of existing works requiring the system to be at steady state at the inspection time. The technique is experimented on a case study and validated through simulation, providing an empirical analysis of its complexity.

Quantitative evaluation of models with stochastic timings can decisively support schedulability analysis and performance engineering of real-time concurrent systems. These tasks require modeling formalisms and solution techniques that can encompass stochastic temporal parameters firmly constrained within a bounded support, thus breaking the limits of Markovian approaches. The problem is further exacerbated by the need to represent suspension of timers, which results from common patterns of real-time programming. This poses relevant challenges both in the theoretical development of non-Markovian solution techniques and in their practical integration within a viable tailoring of industrial processes.

We present an approach for integration of formal methods within an industrial SW process, illustrating results obtained in a real scenario subject to Military Standard 498 (MIL-STD-498). On the one hand, the formal nucleus of preemptive Time Petri Nets (pTPNs) is used to support design and verification activities of the development process; on the other hand, the Unified Modeling Language (UML) profile for Modeling and Analysis of Real-Time and Embedded (MARTE) systems is adopted to manage the documentation process prescribed by MIL-STD-498. The two cores are integrated by providing guidance for translation of UML-MARTE specifications into equivalent pTPN models, with specific reference to concurrency control and synchronization mechanisms. This permits to attain a smooth transition from the standard artifacts of MIL-STD-498 to pTPN models and analyses, facilitating deployment of the formal core of pTPNs with a limited impact on the industrial practice. The experience proves practical feasibility and effectiveness of the approach, comprising a step towards industrial applicability of formal methods and practices.

Hierarchical Scheduling (HS) techniques achieve resource partitioning among a set of real-time applications, providing reduction of complexity, confinement of failure modes, and temporal isolation among system applications. This facilitates compositional analysis for architectural verification and plays a crucial role in all industrial areas where high-performance microprocessors allow growing integration of multiple applications on a single platform. We propose a compositional approach to formal specification and schedulability analysis of real-time applications running under a Time Division Multiplexing (TDM) global scheduler and preemptive Fixed Priority (FP) local schedulers, according to the ARINC-653 standard. As a characterizing trait, each application is made of periodic, sporadic, and jittering tasks with offsets, jitters, and nondeterministic execution times, encompassing intra-application synchronizations through semaphores and mailboxes and interapplication communications among periodic tasks through message passing. The approach leverages the assumption of a TDM partitioning to enable compositional design and analysis based on the model of preemptive Time Petri Nets (pTPNs), which is expressly extended with a concept of Required Interface (RI) that specifies the embedding environment of an application through sequencing and timing constraints. This enables exact verification of intra-application constraints and approximate but safe verification of interapplication constraints. Experimentation illustrates results and validates their applicability on two challenging workloads in the field of safety-critical avionic systems.

In the process of testing of concurrent timed systems, input generation identifies values of temporal parameters that let the Implementation Under Test (IUT) execute selected cases. However, when some parameters are not under control of the driver, test execution may diverge from the selected input and produce an inconclusive behavior. We formulate the problem on the basis of an abstraction of the IUT which we call partially stochastic Time Petri Net (psTPN), where controllable parameters are modeled as nondeterministic values and noncontrollable parameters as random variables with general (GEN) distribution. With reference to this abstraction, we derive the analytical form of the probability that the IUT runs along a selected behavior as a function of choices taken on controllable parameters. In the applicative perspective of real-time testing, this identifies a theoretical upper limit on the probability of a conclusive result, thus providing a means to plan the number of test repetitions that are necessary to guarantee a given probability of test-case coverage. It also provides a constructive technique for an optimal or suboptimal approach to input generation and a way to characterize the probability of conclusive testing under other suboptimal strategies.

Preemptive Time Petri Nets (pTPNs) support modeling and analysis of concurrent timed SW components running under fixed priority preemptive scheduling. The model is supported by a well-established theory based on symbolic state space analysis through Difference Bounds Matrix (DBM) zones, with specific contributions on compositional modularization, trace analysis, and efficient overapproximation and cleanup in the management of suspension deriving from preemptive behavior. In this paper, we devise and implement a framework that brings the theory to application. To this end, we cast the theory into an organic tailoring of design, coding, and testing activities within a V-Model SW life cycle in respect of the principles of regulatory standards applied to the construction of safety-critical SW components. To implement the toolchain subtended by the overall approach into a Model Driven Development (MDD) framework, we complement the theory of state space analysis with methods and techniques supporting semiformal specification and automated compilation into pTPN models and real-time code, measurement-based Execution Time estimation, test case selection and execution, coverage evaluation.

Critical systems require supervising infrastructures to keep their unreliability under control. We propose safety-critical systems to be modeled through a fault-tolerant architecture based on Stochastic Fault Trees (SFTs) and we refer to a scenario where the monitoring infrastructure is a Wireless Sensor Network (WSN). SFTs associate the failure time of leaf events with a non-Markovian (GEN) cumulative distribution function (CDF) and support the evaluation of system unreliability over time. In the reference scenario, the SFT model dynamically updates system unreliability according to samples delivered by the WSN, it maintains a dynamic measure of the safe time-horizon within which the system is expected to operate under a given threshold of unreliability, and it also provides the WSN with a measure of the contribution of each basic event to system unreliability.

Quantitative evaluation of models with generally-distributed transitions requires analysis of non-Markovian processes that may be not isomorphic to their underlying untimed models and may include any number of concurrent non-exponential timers. The analysis of stochastic Time Petri Nets copes with the problem by covering the state space with stochastic-classes, which extend Difference Bounds Matrices (DBM) with a state probability density function. We show that the state-density function accepts a continuous piecewise representation over a partition in DBM-shaped sub-domains. We then develop a closed-form symbolic calculus of state-density functions assuming that model transitions have expolynomial distributions. The calculus shows that within each sub-domain the state-density function is a multivariate expolynomial function and makes explicit how this form evolves through subsequent transitions. This enables an efficient implementation of the analysis process and provides the formal basis that supports introduction of an approximate analysis based on Bernstein Polynomials. The approximation attacks practical and theoretical limits in the applicability of stochastic state-classes, and devises a new approach to the analysis of non Markovian models, relying on approximations in the state space rather than in the structure of the model.

In the verification of reactive systems with nondeterministic densely valued temporal parameters, the state-space can be covered through equivalence classes, each composed of a discrete logical location and a dense variety of clock valuations encoded as a difference bounds matrix (DBM). The reachability relation among such classes enables qualitative verification of properties pertaining events ordering and stimulus/response deadlines, but it does not provide any measure of probability for feasible behaviors. We extend DBM equivalence classes with a density-function which provides a measure for the probability of individual states. To this end, we extend time Petri nets by associating a probability density-function to the static firing interval of each nondeterministic transition. We then explain how this stochastic information induces a probability distribution for the states contained within a DBM class and how this probability evolves in the enumeration of the reachability relation among classes. This enables the construction of a stochastic transition system which supports correctness verification based on the theory of TPNs, provides a measure of probability for each feasible run, enables steady-state analysis based on Markov renewal theory. In so doing, we provide a means to identify feasible behaviors and to associate them with a measure of probability in models with multiple concurrent generally distributed nondeterministic timers.

We describe a methodology for the construction of real-time tasking sets, which smoothly integrates a formal approach in both development and verification processes of the software life cycle. In the design stage, a timeline schema is used to specify concurrent processes with their dependencies and their expected temporal parameters. The schema is automatically translated into an equivalent preemptive time Petri net, which supports verification of the process architecture with respect to timeliness and sequencing requirements through state space analysis. The specification model drives the implementation stage enabling a disciplined coding of the process architecture on top of conventional primitives of a real-time operating system. At the same time, the preemptive Time Petri Net specification and the results of its state space analysis support functional testing enabling the construction of a time-sensitive Oracle and providing a metrics for coverage analysis. Computational experience in the Linux RTAI environment is reported to demonstrate the capability of the method to be effectively integrated in a practical approach.

We address the problem of test case selection and path sensitization in the process of testing real-time preemptive systems, following a formal methodology based on the theory of preemptive Time Petri Nets (pTPN) implemented in the Oris tool. We discuss practical factors that limit feasible behaviors in the implementation of a nondeterministic specification and we motivate the assumption of test cases defined as paths selected in the symbolic state space of a pTPN specification. Feasibility and effectiveness of the proposed sensitization technique are demonstrated through experimentation on a real-time operating system.