Showing 1–26 of 26 results for author: Daszczuk, W B

Cooperation of Multiple Autonomous Robots and Analysis of their Swarm Behavior

Authors: Bogdan Czejdo, Wiktor B. Daszczuk, Waldemar Grabski, Sambit Bhattacharya

Abstract: In this paper, we extended previous studies of cooperating autonomous robots to include situations when environmental changes and changes in the number of robots in the swarm can affect the efficiency to execute tasks assigned to the swarm of robots. We have presented a novel approach based on partition of the robot behavior. The sub-diagrams describing sub-routs allowed us to model advanced inter… ▽ More In this paper, we extended previous studies of cooperating autonomous robots to include situations when environmental changes and changes in the number of robots in the swarm can affect the efficiency to execute tasks assigned to the swarm of robots. We have presented a novel approach based on partition of the robot behavior. The sub-diagrams describing sub-routs allowed us to model advanced interactions between autonomous robots using limited number of state combinations avoiding combinatorial explosion of reachability. We identified the systems for which we can ensure the correctness of robots interactions. New techniques were presented to verify and analyze combined robots' behavior. The partitioned diagrams allowed us to model advanced interactions between autonomous robots and detect irregularities such as deadlocks, lack of termination etc. The techniques were presented to verify and analyze combined robots' behavior using model checking approach. The described system, Dedan verifier, is still under development. In the near future, timed and probabilistic verification are planned. △ Less

Submitted 28 December, 2018; originally announced January 2019.

Comments: 8 pages, 10 figures. arXiv admin note: text overlap with arXiv:1705.04263

MSC Class: 68T40 ACM Class: I.2.9

Journal ref: Autobusy-TEST Vol. 226, 2018, No. 12, pp.872-879

Using Machine Learning to Enhance Vehicles Traffic in ATN (PRT) Systems

Authors: Bogdan Czejdo, Wiktor B. Daszczuk, Mikołaj Baszun

Abstract: This paper discusses new techniques to enhance Automated Transit Networks (ATN, previously called Personal Rapid Transit - PRT) based on Artificial Intelligence tools. The main direction is improvement of the cooperation of autonomous modules that use negotiation protocols, following the IoT paradigm. One of the goals is to increase ATN system throughput by tuning up autonomous vehicles cooperatio… ▽ More This paper discusses new techniques to enhance Automated Transit Networks (ATN, previously called Personal Rapid Transit - PRT) based on Artificial Intelligence tools. The main direction is improvement of the cooperation of autonomous modules that use negotiation protocols, following the IoT paradigm. One of the goals is to increase ATN system throughput by tuning up autonomous vehicles cooperation. Machine learning (ML) was used to improve algorithms designed by human programmers. We used "existing controls" corresponding to near-optimal solutions and built refinement models to more accurately relate a system's dynamics to its performance. A mechanism that mostly influences ATN performance is Empty Vehicle Management (EVM). The algorithms designed by human programmers was used: calls to empty vehicles for waiting passengers and balancing based on reallocation of empty vehicles to achieve better regularity of their settlement. In this paper we discuss how we can improve these algorithms (and tune them to current conditions) by using ML to tailor individual behavioral policies. Using ML techniques was possible because our algorithm is based on a set of parameters. A number of weights and thresholds could be tuned up to give better decisions on moving empty vehicles across the track. △ Less

Submitted 16 December, 2017; originally announced December 2017.

Comments: 6 pages, 3 figures

MSC Class: 68T05 ACM Class: I.2.6

Journal ref: Autobusy-TEST vol. 18(2017), No. 12, pp. 1484-1489

Priority Rules on ATN (PRT) Intersections

Authors: Waldemar Grabski, Wiktor B. Daszczuk

Abstract: In Autonomous Transit Networks some basic elements influence the throughput: network structure, maximum velocity, number of vehicles etc. Other parameters like station structure, dynamic routing or vehicle behavior on intersections play minor role. Yet in highly congested nets, when vehicles interfere in the traffic, some subtle decisions may influence overall system ridership. We tested the impac… ▽ More In Autonomous Transit Networks some basic elements influence the throughput: network structure, maximum velocity, number of vehicles etc. Other parameters like station structure, dynamic routing or vehicle behavior on intersections play minor role. Yet in highly congested nets, when vehicles interfere in the traffic, some subtle decisions may influence overall system ridership. We tested the impact of intersection priority rules on passenger waiting time, which measures the throughput. The dependence occurred its relevance in a crowded network. △ Less

Submitted 16 December, 2017; originally announced December 2017.

Comments: 4 pages, 4 figures, 1 table

MSC Class: 68U20 ACM Class: I.6.3

Journal ref: Autobusy-TEST vol. 18(2017), No. 12, pp. 1503-1506

Critical trees: counterexamples in model checking of CSM systems using CBS algorithm

Authors: Wiktor B. Daszczuk

Abstract: The important feature of temporal model checking is the generation of counterexamples. In the report, the requirements for generation of counterexample (called critical tree) in model checking of CSM systems are described. The output of TempoRG model checker for QsCTL logic (a version of CTL) is presented. A contradiction between counterexample generation and state space reduction is commented. The important feature of temporal model checking is the generation of counterexamples. In the report, the requirements for generation of counterexample (called critical tree) in model checking of CSM systems are described. The output of TempoRG model checker for QsCTL logic (a version of CTL) is presented. A contradiction between counterexample generation and state space reduction is commented. △ Less

Submitted 26 October, 2017; originally announced October 2017.

Comments: 20 pages, 12 figures

Report number: ICS WUT Research Report No 8/2002 MSC Class: 68N30 ACM Class: D.2.4

Verification of Design Decisions in Communication Protocol by Evaluation of Temporal Logic Formulas

Authors: Wiktor B. Daszczuk

Abstract: During the project of a communication protocol, many design decisions influence the behavior of the protocol and its correctness. Formal specification and verification of the protocol may prove its correctness. In this paper, an example of a verification of design decision using formal specification in CSM automata and verification in temporal logic is presented. During the project of a communication protocol, many design decisions influence the behavior of the protocol and its correctness. Formal specification and verification of the protocol may prove its correctness. In this paper, an example of a verification of design decision using formal specification in CSM automata and verification in temporal logic is presented. △ Less

Submitted 25 October, 2017; originally announced October 2017.

Comments: 15 pages, 7 figures

Report number: ICS WUT Research Report 22/98 MSC Class: 68N30 ACM Class: D.2.4

State Space Reduction for Reachability Graph of CSM Automata

Authors: Wiktor B. Daszczuk

Abstract: Classical CTL temporal logics are built over systems with interleaving model concurrency. Many attempts are made to fight a state space explosion problem (for instance, compositional model checking). There are some methods of reduction of a state space based on independence of actions. However, in CSM model, which is based on coincidences rather than on interleaving, independence of actions cannot… ▽ More Classical CTL temporal logics are built over systems with interleaving model concurrency. Many attempts are made to fight a state space explosion problem (for instance, compositional model checking). There are some methods of reduction of a state space based on independence of actions. However, in CSM model, which is based on coincidences rather than on interleaving, independence of actions cannot be defined. Therefore a state space reduction basing on identical temporal consequences rather than on independence of action is proposed. The new reduction is not as good as for interleaving systems, because all successors of a state (in depth of two levels) must be obtained before a reduction may be applied. This leads to reduction of space required for representation of a state space, but not in time of state space construction. Yet much savings may occur in regular state spaces for CSM systems. △ Less

Submitted 25 October, 2017; originally announced October 2017.

Comments: 12 pages, 10 figures

Report number: ICS WUT Research Report No 10/2000 MSC Class: 68N30 ACM Class: D.2.2

JADE - A Platform for Research on Cooperation of Physical and Virtual Agents

Authors: Wiktor B. Daszczuk, Jerzy Mieścicki

Abstract: In the ICS, WUT a platform for simulation of cooperation of physical and virtual mobile agents is under development. The paper describes the motivation of the research, an organization of the platform, a model of agent, and the principles of design of the platform. Several experimental simulations are briefly described. In the ICS, WUT a platform for simulation of cooperation of physical and virtual mobile agents is under development. The paper describes the motivation of the research, an organization of the platform, a model of agent, and the principles of design of the platform. Several experimental simulations are briefly described. △ Less

Submitted 24 October, 2017; originally announced October 2017.

Comments: 7 pages, 6 figures

Report number: ICS WUT Research Report No 15/2001 MSC Class: 68T42 ACM Class: C.2.0

Macrogeneration and Automata Libraries For COSMA design environment

Authors: Wiktor B. Daszczuk

Abstract: In ICS, WUT a COSMA design environment is being developed. COSMA is based on Concurrent State Machines (CSM) formalism of system specification. It contains a graphical tool for system design, various tools for the analysis (including a temporal model checker), simulator and code generator. In many projects, some common susbsystems take place. This concerns both complicated modules and simple count… ▽ More In ICS, WUT a COSMA design environment is being developed. COSMA is based on Concurrent State Machines (CSM) formalism of system specification. It contains a graphical tool for system design, various tools for the analysis (including a temporal model checker), simulator and code generator. In many projects, some common susbsystems take place. This concerns both complicated modules and simple counters. In the report, a concept of macrogeneration technique for building of libraries of automata is presented. The new technique will support a compactness of projects and reusability of modules. △ Less

Submitted 24 October, 2017; originally announced October 2017.

Comments: 26 pages, 14 figures

Report number: ICS WUT Research Report No 7/2003 MSC Class: 68N30 ACM Class: D.2.2

Deadlock and Termination Detection using IMDS Formalism and Model Checking. Version 2

Authors: Wiktor B. Daszczuk

Abstract: Modern model checking techniques concentrate on global properties of verified systems, because the methods base on global state space. Local features like partial deadlock or process termination are not easy to express and check. In the paper a description of distributed system in an Integrated Model of Distributed Systems (IMDS) combined with model checking is presented. IMDS expresses a dualism… ▽ More Modern model checking techniques concentrate on global properties of verified systems, because the methods base on global state space. Local features like partial deadlock or process termination are not easy to express and check. In the paper a description of distributed system in an Integrated Model of Distributed Systems (IMDS) combined with model checking is presented. IMDS expresses a dualism in distributed systems: server view and agent view. The formalism uses server states and messages. A progress in computations is defined in terms of actions consuming and producing states and messages. Distributed actions are totally independent and they do not depend on global state. Therefore, IMDS allows the designer to express local features of subsystems. In this model it is easy to describe various kinds of deadlock (including partial deadlock) and to differentiate deadlock from termination. The integration of IMDS with model checking is presented. Temporal formulas testing various kinds of deadlock (in communication or over resources) and termination are proposed. △ Less

Submitted 24 October, 2017; originally announced October 2017.

Comments: 18 pages

Report number: ICS WUT Research Report No. 2/2008 MSC Class: 68Q85 ACM Class: F.1.1

Timed Concurrent State Machines

Authors: Wiktor B. Daszczuk

Abstract: Timed Concurrent State Machines are an application of Alur's Timed Automata concept to coincidence-based (rather than interleaving) CSM modeling technique. TCSM support the idea of testing automata, allowing to specify time properties easier than temporal formulas. Also, calculation of a global state space in real-time domain (Region Concurrent State Machines) is defined, allowing to store a verif… ▽ More Timed Concurrent State Machines are an application of Alur's Timed Automata concept to coincidence-based (rather than interleaving) CSM modeling technique. TCSM support the idea of testing automata, allowing to specify time properties easier than temporal formulas. Also, calculation of a global state space in real-time domain (Region Concurrent State Machines) is defined, allowing to store a verified system in ready-to-verification form, and to multiply it by various testing automata. △ Less

Submitted 22 October, 2017; originally announced October 2017.

Comments: 13 pages, 4 figures

MSC Class: 68Q85 ACM Class: F.1.1

Journal ref: Computer Science, vol. 8, 2007, pp. 23-36

Communication Dualism in Distributed Systems with Petri Net Interpretation

Authors: Stanisław Chrobot, Wiktor B. Daszczuk

Abstract: In the paper notion of communication dualism id formalized and explained in Petri net interpretation. We consider communication dualism a basic property of communication in distributed systems. The formalization is done in the Integrated Model of Distributed Systems (IMDS) where synchronous communication, as well as asynchronous message-passing and variable-sharing are modeled in a common framewor… ▽ More In the paper notion of communication dualism id formalized and explained in Petri net interpretation. We consider communication dualism a basic property of communication in distributed systems. The formalization is done in the Integrated Model of Distributed Systems (IMDS) where synchronous communication, as well as asynchronous message-passing and variable-sharing are modeled in a common framework. In the light of this property, communication in distributed systems can be seen as a two-dimensional phenomenon with passing being its spatial dimension and sharing its temporal dimension. Any distributed system can be modeled as a composition of message-passes asynchronous processes or as a composition of variable-sharing asynchronous processes. A method of automatic process extraction in Petri net interpretation of IMDS is presented. △ Less

Submitted 22 October, 2017; originally announced October 2017.

Comments: 14 pages, 4 figures, Appendix with proofs of some lemmas

MSC Class: 68Q85 ACM Class: F.1.1

Journal ref: Theoretical and Applied Informatics vol. 4/2006, pp. 261-278, ISSN: 1896-5334

Distributed algorithm for empty vehicles management in personal rapid transit (PRT) network

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

Abstract: 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… ▽ More 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. △ Less

Submitted 17 October, 2017; originally announced October 2017.

Comments: 22 pages, 6 figures, 5 tables

MSC Class: 37M05 ACM Class: I.6.3

Journal ref: Journal of Advanced Transportation, vol. 50 (2016), No.4, pp.608-629

Proposed benchmarks for PRT networks simulation

Authors: Jerzy Mieścicki, Wiktor B. Daszczuk

Abstract: Personal Rapid Transit (PRT) is a promising form of urban transport. Its operation consists in the use of small unmanned vehicles which convey the passengers among stations within a dedicated network. Various aspects of the PRT network performance are frequently evaluated using the discrete-event simulation. The paper supports the need of establishing some reference models for the simulation of PR… ▽ More Personal Rapid Transit (PRT) is a promising form of urban transport. Its operation consists in the use of small unmanned vehicles which convey the passengers among stations within a dedicated network. Various aspects of the PRT network performance are frequently evaluated using the discrete-event simulation. The paper supports the need of establishing some reference models for the simulation of PRT networks, targeted mainly towards the needs of the research on network management algorithms. Three models of such PRT network models are proposed and discussed. The presented models can play the role of benchmarks which would be very useful for comparative evaluation of heuristic control algorithms, developed by different research groups. △ Less

Submitted 13 October, 2017; originally announced October 2017.

Comments: 11 pages, 5 figures

MSC Class: 00A72 ACM Class: I.6.5

Journal ref: Archives of Transport, vol. 27-28, nr 3-4, 2013, pp.123-133

Threefold Analysis of Distributed Systems: IMDS, Petri Net and Distributed Automata DA3

Authors: Wiktor B. Daszczuk

Abstract: Integrated Model of Distributed Systems is used for specification and verification of distributed systems. In the formalism, a system is modeled as a set of servers' states and agents' messages. The operation of a system is modeled as actions converting global system configuration (a set of states and messages) to a new configuration. The formalism is used in Dedan verification environment, in whi… ▽ More Integrated Model of Distributed Systems is used for specification and verification of distributed systems. In the formalism, a system is modeled as a set of servers' states and agents' messages. The operation of a system is modeled as actions converting global system configuration (a set of states and messages) to a new configuration. The formalism is used in Dedan verification environment, in which specification and verification of distributed systems is performed. Equivalent Petri nets are used for structural analysis. For the graphical specification and simulation of distributed systems, Distributed Autonomous and Asynchronous Automata (DA3) are invented. Such simulation does not require calculation of global configuration space of a system. Two forms of DA3 are shown: Server-DA3 (SDA3) for the server view and Agent-DA3 (ADA3) for the agent view. △ Less

Submitted 9 October, 2017; originally announced October 2017.

Comments: 10 pages, 5 figures, 1 table

MSC Class: 68Q85 ACM Class: D.1.3

Journal ref: The 37th IEEE Software Engineering Workshop, Federated Conference on Computer Science and Information Systems, SEW-37, FedCSIS 2017, Prague, Czech Republic, 3-6 September 2017, pp. 377-386

Rybu: Imperative-style Preprocessor for Verification of Distributed Systems in the Dedan Environment

Authors: Wiktor B. Daszczuk, Maciej Bielecki, Jan Michalski

Abstract: Integrated Model of Distributed Systems (IMDS) is developed for specification and verification of distributed systems, and verification against deadlocks. On the basis of IMDS, Dedan verification environment was prepared. Universal deadlock detection formulas allow for automatic verification, without any knowledge of a temporal logic, which simplifies the verification process. However, the input l… ▽ More Integrated Model of Distributed Systems (IMDS) is developed for specification and verification of distributed systems, and verification against deadlocks. On the basis of IMDS, Dedan verification environment was prepared. Universal deadlock detection formulas allow for automatic verification, without any knowledge of a temporal logic, which simplifies the verification process. However, the input language, following the rules of IMDS, seems to be exotic for many users. For this reason Rybu preprocessor was created. Its purpose is to build large models in imperative-style language, on much higher abstraction level. △ Less

Submitted 7 October, 2017; originally announced October 2017.

Comments: 16 pages, 1 figure

MSC Class: 68Q85 ACM Class: D.1.3

Journal ref: KKIO 2017 - Software Engineering Conference, Rzeszów, Poland, 14-16 Sept 2017, Software Engineering Research for the Practice, Polish Information Processing Society, pp. 135-150

Practical Approach to Distributed Systems' Design

Authors: Jerzy Mieścicki, Wiktor B. Daszczuk, Waldemar Grabski, Artur Krystosik

Abstract: The paper, based on authors' experience from several distributed systems integration projects, summarizes briefly practical designer's view on methodological requirements and overall system organization, including clues as to the organization of the application layer, use of operating system and preferred communication protocols. The paper, based on authors' experience from several distributed systems integration projects, summarizes briefly practical designer's view on methodological requirements and overall system organization, including clues as to the organization of the application layer, use of operating system and preferred communication protocols. △ Less

Submitted 16 May, 2017; originally announced July 2017.

MSC Class: 68M14 ACM Class: C.1.4

Journal ref: Scientific Journal of Silesian University of Technology. Series Computer Science. Vol. 34, Proc. V Seminar "Computer Networks", 18-19 March 1998, Gliwice, Poland, pp. 205-214

Discrete Event Simulation of Personal Rapid Transit (PRT) Systems

Authors: Wiktor B. Daszczuk

Abstract: The article discusses issues related to the construction of the PRT network simulator and the simulation process: the elements of PRT network structure, their representation in the simulator, the simulation process itself, animation, and automation of the experiments. An example of a simulation environment Feniks is described, elaborated within the framework of the Eco-Mobility project. The article discusses issues related to the construction of the PRT network simulator and the simulation process: the elements of PRT network structure, their representation in the simulator, the simulation process itself, animation, and automation of the experiments. An example of a simulation environment Feniks is described, elaborated within the framework of the Eco-Mobility project. △ Less

Submitted 12 May, 2017; originally announced May 2017.

Comments: 12 pages, 3 figures

MSC Class: 68U20 ACM Class: I.6.8

Journal ref: Autobusy-TEST, vol. 17(2016), No.3, pp.1302-1310

Model Checking in The COSMA Environment as a Support for The Design of Pipelined Processing

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

Abstract: 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. 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. △ Less

Submitted 12 May, 2017; originally announced May 2017.

Comments: 15 pages, 11 figures, European Congress on Computational Methods in Applied Sciences and Engineering ECCOMAS 2004, Jyväskylä, Finland, 24-28 July 2004

MSC Class: 68U07 ACM Class: D.2.10

Distributed management of Personal Rapid Transit (PRT) vehicles under unusual transport conditions

Authors: Wiktor B. Daszczuk, Jerzy Mieścicki

Abstract: 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 basin… ▽ More 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. △ Less

Submitted 12 May, 2017; originally announced May 2017.

Comments: 6 pages, 1 figure, 3 tables

MSC Class: 68U20 ACM Class: C.2.4

Journal ref: Logistyka Vol. 4/2015, pp. 2896-2901

Improving Resilience of Autonomous Moving Platforms by Real Time Analysis of Their Cooperation

Authors: Bogdan Czejdo, Sambit Bhattacharya, Mikołaj Baszun, Wiktor B. Daszczuk

Abstract: Environmental changes, failures, collisions or even terrorist attacks can cause serious malfunctions of the delivery systems. We have presented a novel approach improving resilience of Autonomous Moving Platforms AMPs. The approach is based on multi-level state diagrams describing environmental trigger specifications, movement actions and synchronization primitives. The upper level diagrams allowe… ▽ More Environmental changes, failures, collisions or even terrorist attacks can cause serious malfunctions of the delivery systems. We have presented a novel approach improving resilience of Autonomous Moving Platforms AMPs. The approach is based on multi-level state diagrams describing environmental trigger specifications, movement actions and synchronization primitives. The upper level diagrams allowed us to model advanced interactions between autonomous AMPs and detect irregularities such as deadlocks live-locks etc. The techniques were presented to verify and analyze combined AMPs' behaviors using model checking technique. The described system, Dedan verifier, is still under development. In the near future, a graphical form of verified system representation is planned. △ Less

Submitted 11 May, 2017; originally announced May 2017.

Comments: 11 pages, 5 figures

MSC Class: 68U07 ACM Class: D.2.4

Journal ref: Autobusy-TEST, vol. 17, No.3, pp.1294-1301 (2016)

Verification of Concurrent Engineering Software Using CSM Models

Authors: Jerzy Mieścicki, Mikołaj Baszun, Wiktor B. Daszczuk, Bogdan D. Czejdo

Abstract: 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 inte… ▽ More 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. △ Less

Submitted 20 April, 2017; originally announced April 2017.

Comments: 9 pages, 12 figures

MSC Class: 68N30 ACM Class: D.2.2

Journal ref: Proc.2nd World Conf. on Integrated Design and Process Technology, Austin, Texas, USA, December 1-4, 1996, Vol. 2, pp.322-330

Concurrent Software Design Based on Constraints on State Diagrams

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

Abstract: 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 C… ▽ More 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. △ Less

Submitted 23 March, 2017; originally announced March 2017.

Comments: 17 pages, 12 figures, 3rd Biennial World Conference on Integrated Design & Process Technology, Berlin, July 6-9, 1998

MSC Class: 68N30 ACM Class: D.2.10

System level specification and verification using Concurrent State Machines and COSMA environment

Authors: Wiktor B. Daszczuk, Jerzy Mieścicki, Michał Nowacki, Jacek Wytrębowicz

Abstract: 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 intr… ▽ More 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. △ Less

Submitted 16 March, 2017; originally announced March 2017.

Comments: 16 pages, 8 figures

MSC Class: 68M01 ACM Class: B.6.3

Journal ref: Proc. 8th International Conference on Mixed Design of Integrated Circuits and Systems MIXDES 2001, June 21-23, Zakopane, Poland, pp. 525-532

Behavioral an real-time verification of a pipeline in the COSMA environment

Authors: Jerzy Mieścicki, Wiktor B. Daszczuk

Abstract: 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… ▽ More 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. △ Less

Submitted 16 March, 2017; originally announced March 2017.

Comments: 12 pages, 7 figures

MSC Class: 68M14 ACM Class: B.1.4

Journal ref: Annales UMCS, Informatica AI v. 4 (2006), pp. 254-265

Evaluation of Temporal Formulas Based on "Checking By Spheres"

Authors: Wiktor B. Daszczuk

Abstract: Classical algorithms of evaluation of temporal CTL formulas are constructed "bottom-up". A formula must be evaluated completely to give the result. In the paper, a new concept of "top-down" evaluation of temporal QsCTL (CTL with state quantifiers) formulas, called "Checking By Spheres" is presented. The new algorithm has two general advantages: the evaluation may be stopped on certain conditions i… ▽ More Classical algorithms of evaluation of temporal CTL formulas are constructed "bottom-up". A formula must be evaluated completely to give the result. In the paper, a new concept of "top-down" evaluation of temporal QsCTL (CTL with state quantifiers) formulas, called "Checking By Spheres" is presented. The new algorithm has two general advantages: the evaluation may be stopped on certain conditions in early steps of the algorithm (not the whole formula and not whole state space should be analyzed), and state quantification may be used in formulas (even if a range of a quantifier is not statically obtainable). △ Less

Submitted 12 February, 2017; originally announced February 2017.

Comments: 7 pages, 7 figures

ACM Class: D.2.4

Journal ref: Proc. Euromicro Symposium on Digital Systems Design - Architectures, Methods and Tools, September 4-6 2001, Warsaw, Poland, pp. 158-164

System Modeling in the COSMA Environment

Authors: Wiktor B. Daszczuk, Waldemar Grabski, Jerzy Mieścicki, Jacek Wytrębowicz

Abstract: The aim of this paper is to demonstrate how the COSMA environment can be used for system modeling. This environment is a set of tools based on Concurrent State Machines paradigm and is developed in the Institute of Computer Science at the Warsaw University of Technology. Our demonstration example is a distributed brake control system dedicated for a railway transport. The paper shortly introduces… ▽ More The aim of this paper is to demonstrate how the COSMA environment can be used for system modeling. This environment is a set of tools based on Concurrent State Machines paradigm and is developed in the Institute of Computer Science at the Warsaw University of Technology. Our demonstration example is a distributed brake control system dedicated for a railway transport. The paper shortly introduces COSMA. Next it shows how the example model can be validated by our temporal logic analyzer. △ Less

Submitted 12 February, 2017; originally announced February 2017.

Comments: 6 pages, 3 figures, 1 table

Journal ref: Proc. Euromicro Symposium on Digital Systems Design - Architectures, Methods and Tools, September 4-6 2001, Warsaw, Poland, pp. 152-157