This paper is devoted to the problem of designing a computational system utilizing the minimal number of processors to ensure that the program is executed before the deadline. The program is represented by a direct acyclic graph where vertices correspond to jobs. The system is supposed to tolerate both hardware and software faults. The schedule of the program execution does not include the exact moments of job launch and termination, thus allowing to employ abstract models with various levels of detail to estimate the time of execution. A simulated annealing algorithm is proposed for this problem. The paper provides the proof of asymptotic convergence of the algorithm and an experimental evaluation. The algorithm is also applied to a practical problem of scheduling in radiolocation systems.

Checking the correctness of distributed systems is one of the most difficult and urgent problems in software engineering. A combined toolset for the verification of real-time distributed systems (RTDS) is described. RTDSs are specified as statecharts in the Universal Modeling Language (UML). The semantics of statecharts is defined by means of hierarchical timed automata. The combined toolset consists of a UML statechart editor, a verification tool for model checking networks of real-time automata in UPPAAL, and a translator of UML statecharts into networks of timed automata. The focus is on the translation algorithm from UML statecharts into networks of hierarchical timed automata. To illustrate the proposed approach to the verification of RTDSs, a toy example of a real-time crossroad traffic control system is analyzed.

To verify real-time properties of UML statecharts one may apply a UPPAAL, toolbox for model checking of real-time systems. One of the most suitable ways to specify an operational semantics of UML statecharts is to invoke the formal model of Hierarchical Timed Automata. Since the model language of UPPAAL is based on Networks of Timed Automata one has to provide a conversion of Hierarchical Timed Automata to Networks of Timed Automata. In this paper we describe this conversion algorithm and prove that it is correct w.r.t. UPPAAL query language which is based on the subset of Timed CTL.

An algorithm was proposed to simulate annealing for determination of the minimal necessary number of processors and construction of the static schedule for execution of the applied programs with allowance for the constraints on the time of schedule execution and reliability requirements. The developed algorithm was substantiated both theoretically and experimentally by comparing different laws of temperature decrease in the annealing simulation algorithm.

This paper describes a method of designing a computational system with the minimal number of processors. Strict execution deadlines apply, as well as restrictions on the reliability of the system that imply the tolerance of the system to both hardware and software faults. The problem is formulated mathematically, an algorithm of solution based on simulated annealing is described, and experimental results are shown.

To verify real-time properties of UML statecharts one may apply a UPPAAL, toolbox for model checking of real-time systems. One of the most suitable ways to specify an operational semantics of UML statecharts is to invoke the formal model of Hierarchical Timed Automata. Since the model language of UPPAAL is based on Networks of Timed Automata one has to provide a conversion of Hierarchical Timed Automata to Networks of Timed Automata. In this paper we describe this conversion algorithm and prove that it is correct w.r.t. UPPAAL query language which is based on the subset of Timed CTL.

In this paper we present DYANA, an HLA-based hardware-in-the-loop simulation tool. This tool is used for distributed Real-Time Embedded Systems (RTES) simulation. RTES models are described by Unified Modeling Language (UML) statechart diagrams. The statechart diagram is transformed into HLA-based Simulation Model (HSM). After translation into HSM we use CERTI as the simulation runtime. The statechart diagram is also transformed into a Network of Timed Automata (NTA). After translation into NTA we use UPPAAL for RTES model verification.

This paper describes a method of designing a computational system with the minimal number of processors. Strict execution deadlines apply, as well as restrictions on the reliability of the system that imply the tolerance of the system to both hardware and software faults. The problem is formulated mathematically, an algorithm of solution based on simulated annealing is described, and experimental results are shown.

DYANA 1 is an environment designed for development of distributed systems. We demonstrate that DYANA augmented with UPPAAL is well suited for simulation and model checking of real-time embedded system designs defined with UML statecharts. To this end, we present the case studies of onboard systems for cars and aircrafts as well as of a general-purpose fault-tolerant system for running parallel programs. For each case study we give its informal description, specify a formal model defined with UML diagrams and report on the simulation and model checking results.