Abstract The use of formal methods to prove the correctness of compositional embedded systems is increasingly important. However, the required models and algorithms can induce an enormous complexity. Our approach divides the formal system model into layers and these in turn into modules with defined interfaces, so that reduced formal models can be created for the verification of concrete functional and non-functional requirements. In this work, we use Uppaal to (1) model an RTOS kernel in a modular way and formally specify its internal requirements, (2) model abstract tasks that trigger all kernel functionalities in all combinations or scenarios, and (3) verify the resulting system with regard to task synchronization, resource management, and timing. The result is a fully verified model of the operating system layer that can henceforth serve as a dependable foundation for verifying compositional applications w.r.t. various aspects, such as timing or liveness.

Abstract The architecture of ARINC-653 partitioned scheduling has been widely applied to avionics systems owing to its robust temporal isolation among applications. However, this partitioning mechanism causes the problem of how to optimize the partition scheduling of a complex system while guaranteeing its schedulability. In this paper, a model-based optimization approach is proposed. We formulate the problem as a parameter sweep application, which searches for the optimal partition scheduling parameters with respect to minimum processor occupancy via an evolutionary algorithm. An ARINC-653 partitioned scheduling system is modeled as a set of timed automata in the model checker UPPAAL. The optimizer tentatively assigns parameter settings to the models and subsequently invokes UPPAAL to verify schedulability as well as evaluate promising solutions. The parameter space is explored with an evolutionary algorithm that combines refined genetic operators and the self-adaptation of evolution strategies. The experimental results show the applicability of our optimization method.

Different scheduling algorithms for mixed criticality systems have been recently proposed. The common denominator of these algorithms is to discard low critical tasks whenever high critical tasks are in lack of computation resources. This is achieved upon a switch of the scheduling mode from Normal to Critical. We distinguish two main categories of the algorithms: system-level mode switch and task-level mode switch. System-level mode algorithms allow low criticality (LC) tasks to execute only in normal mode. Task-level mode switch algorithms enable to switch the mode of an individual high criticality task (HC), from low (LO) to high (HI), to obtain priority over all LC tasks. This paper investigates an online scheduling algorithm for mixed-criticality systems that supports dynamic mode switches for both task level and system level. When a HC task job overruns its LC budget, then only that particular job is switched to HI mode. If the job cannot be accommodated, then the system switches to Critical mode. To accommodate for resource availability of the HC jobs, the LC tasks are degraded by stretching their periods until the Critical mode exhibiting job complete its execution. The stretching will be carried out until the resource availability is met. We have mechanized and implemented the proposed algorithm using Uppaal. To study the efficiency of our scheduling algorithm, we examine a case study and compare our results to the state of the art algorithms.

We present a compositional framework for the specification and analysis of hierarchical scheduling systems (HSS). Firstly we provide a generic formal model, which can be used to describe any type of scheduling system. The concept of Job automata is introduced in order to model job instantiation patterns. We model the interaction between different levels in the hierarchy through the use of state-based resource models. Our notion of resource model is general enough to capture multi-core architectures, preemptiveness and non-determinism.

While standalone tools for verification and modeling have proven useful, their chosen formalism and description-language can at times be restrictive. We demonstrate how to use U PPAAL SMC to analyze controller systems consisting of Function Mockup Units (FMU) modeled in other tools, such as Matlab and Modelica. Apart from supporting FMI-FMU modules the newly added C interface can call any external function. The only requirement for sound analysis is statelessness and determinism of the external function. We demonstrate the expressive power by implementing the FMI-FMU master algorithm as a timed automata, interfacing with external, non-native and non-trivial Function Mockup Units (FMU). We also model two components in U PPAAL SMC exporting one of them as an FMU while keeping the other as a native component. Furthermore we demonstrate the first simulation environment for the Function Mockup Units, capable of checking bounded MITL properties.

An energy management system of a microgrid (MG) has several basic objectives; e.g. to maximize the utilization of renewable energy resources (RES), to protect the internal components from overloading, and to ensure that the MG operates reliably under any operating conditions. Although many control techniques are available in the literature to monitor and control the energy flows among distributed RES in MGs, formal verification of those techniques was not proposed yet. The emphasis of this paper is to design and validate energy management system for a MG which consists of a solar photovoltaic (PV) array, a pair of battery energy storage systems (BESes), a diesel generator (DG) and a load (LD). The physics and dynamics of the MG are defined as energy flow invariants and the designed behaviours are abstracted, modelled and validated in this work. Therefore, we have considered an invariant based flow technique to manage the energy flow in an MG. The results are validated and verified with UPPAAL, a powerful industrial tool which is commonly used to verify the correctness of real-time systems like supervisory controllers, communication protocols and others.

The analysis of probabilistic schedulability explores all possible combinations of the probabilities of task attributes, which can easily lead to exponential computation time [24]. In this paper, we present a flexible schedulability analysis framework for periodic and sporadic tasks having probabilistic attributes where the computation time scales linearly in the size of analyzed systems. The framework is given in terms of a set of Parameterized Stopwatch Automata (PSA) models, which leads to a large degree of flexibility. Probability distributions for response time are generated using statistical model checking (UPPAAL SMC) while the overall schedulability can be checked using symbolic model checking (UPPAAL). We also define PoMD (percentage of missed deadlines) as a measure of the probabilistic schedulability of systems. To evaluate our approach, we compare the time used for computing response times and the analysis results using similar task models to that of a related analytical approach.

This paper presents a new process algebra, called PACOR, for real-time systems which deals with resource constrained timed behavior as an improved version of the ACSR algebra. We define PACOR as a Process Algebra of Communicating Resources which allows to express preemptiveness, urgent ness and resource usage over a dense-time model. The semantic interpretation of PACOR is defined in the form of a timed transition system expressing the timed behavior and dynamic creation of processes. We define a translation of PACOR systems to Parameterized Stopwatch Automata (PSA). The translation preserves the original semantics of PACOR and enables the verification of PACOR systems using symbolic model checking in UPPAAL and statistical model checking UPPAAL SMC. Finally we provide an example to illustrate system specification in PACOR, translation and verification.

We present the concept of degree of schedulability for mixed-criticality scheduling systems. This concept is given in terms of the two factors 1) Percentage of Missed Deadlines (PoMD), and 2) Degradation of the Quality of Service (DoQoS). The novel aspect is that we consider task arrival patterns that follow user-defined continuous probability distributions. We determine the degree of schedulability of a single scheduling component which can contain both periodic and sporadic tasks using statistical model checking in the form of UPPAAL SMC. We support uniform, exponential, Gaussian and any user-defined probability distribution.

A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation and a set of operators supporting stepwise design.We develop a complete specification framework for real-time systems using Timed I/O Automata as the specification formalism, with the semantics expressed in terms of Timed I/O Transition Systems.We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications -all indispensable ingredients of a compositional design methodology.The theory is implemented on top of an engine for timed games, Uppaal-tiga, and illustrated with a small case study.

Modal and mixed transition systems are specification formalisms that allow the mixing of over- and under-approximation. We discuss three fundamental decision problems for such specifications: — whether a set of specifications has a common implementation; — whether an individual specification has an implementation; and — whether all implementations of an individual specification are implementations of another one. For each of these decision problems we investigate the worst-case computational complexity for the modal and mixed cases. We show that the first decision problem is EXPTIME-complete for both modal and mixed specifications. We prove that the second decision problem is EXPTIME-complete for mixed specifications (it is known to be trivial for modal ones). The third decision problem is also shown to be EXPTIME-complete for mixed specifications.