Jerzy Mieścicki

Wiktor B. Daszczuk, Jerzy Mieścicki

The paper presents a flexibility of management of vehicles in Personal Rapid Transit (PRT) network. The algorithm used for delivering empty vehicles for waiting passengers is based on multiparameter analysis. Due to its distributed construction, the algorithm has a horizon parameter, which specifies the maximum distance between stations the communications is performed. Every decision is made basing on an information about situation (number of vehicles standing at a station, number of vehicles travelling to a station, number of passengers waiting) sent between stations, without any central data base containing traffic conditions. The simulation of the traffic in random case (typical) and in unusual case of delivering people to a social event occurring at single place is presented. It is shown that simple manipulation with horizon parameter allows to adapt the network to extremely uneven demand and destination choice.

Wiktor B. Daszczuk, Jerzy Mieścicki, Waldemar Grabski

In this paper, an original heuristic algorithm of empty vehicles management in personal rapid transit network is presented. The algorithm is used for the delivery of empty vehicles for waiting passengers, for balancing the distribution of empty vehicles within the network, and for providing an empty space for vehicles approaching a station. Each of these tasks involves a decision on the trip that has to be done by a selected empty vehicle from its actual location to some determined destination. The decisions are based on a multi-parameter function involving a set of factors and thresholds. An important feature of the algorithm is that it does not use any central database of passenger input (demand) and locations of free vehicles. Instead, it is based on the local exchange of data between stations: on their states and on the vehicles they expect. Therefore, it seems well-tailored for a distributed implementation. The algorithm is uniform, meaning that the same basic procedure is used for multiple tasks using a task-specific set of parameters.

Jerzy Mieścicki, Bogdan Czejdo, Wiktor B. Daszczuk

The case study analyzed in the report involves the behavioral specification and verification of a three-stage pipeline consisting of mutually concurrent modules which also compete for a shared resource. The system components are specified in terms of Concurrent State Machines (CSM) and the verification technique used is the temporal model checking in the COSMA environment.

Jerzy Mieścicki, Mikołaj Baszun, Wiktor B. Daszczuk et al.

An engineering design process may involve software modules that can executed concurrently. Concurrent modules can be very easily subject to some synchronization errors. This paper discusses verification process for such engineering software. We present a method for verification that requires several steps. First, the state diagram models are constructed that describe the design iterations and interactions with the designer. Next, the state diagram models are transformed into concurrent state machines (CSM). After that, the CSM models are analyzed in order to verify their correctness. In this phase, the modifications are performed in necessary. In the last phase the code is generated. The tools to support our method can be called new concurrent CASE tools. Using these tools the engineering software can be created that is verified for correctness in respect to concurrent execution.

Bogdan D. Czejdo, Wiktor B. Daszczuk, Jerzy Mieścicki

Concurrent software for engineering computations consists of multiple cooperating modules. The behavior of individual modules is described by means on state diagrams. In the paper, the constraints on state diagrams are proposed, allowing for the specification of designer's intentions as to the synchronization of modules. Also, the translation of state diagrams (with enforcement constraints) into Concurrent State Machines is shown, which provides formal framework for the verification of inter-module synchronization. An example of engineering software design based on the method is presented.

Wiktor B. Daszczuk, Jerzy Mieścicki, Michał Nowacki et al.

Traffic Light Controller, a typical benchmark device, is specified and verified using of a formal model called Concurrent State Machines (CSM) and the software environment COSMA 2.0, which supports the system level specification and analysis of concurrent, asynchronous and communicating units. The TLC itself is a system of three concurrent components (the controller and two timers). The paper introduces briefly the CSM model and illustrates how system components are specified, how the reachability graph of a system is obtained and how the requirements are formally verified. Finally, the hints for the generation of VHDL code for the TLC are given.

Jerzy Mieścicki, Wiktor B. Daszczuk

The case study analyzed in the paper illustrates the example of model checking in the COSMA environment. The system itself is a three-stage pipeline consisting of mutually concurrent modules which also compete for a shared resource. System components are specified in terms of Concurrent State Machines (CSM) The paper shows verification of behavioral properties, model reduction technique, analysis of counter-example and checking of real time properties.