On the expressive power of behavioral profiles

Behavioral profiles have been proposed as a behavioral abstraction of dynamic systems, specifically in the context of business process modeling. A behavioral profile can be seen as a complete graph over a set of task labels, where each edge is annotated with one relation from a given set of binary behavioral relations. Since their introduction, behavioral profiles were argued to provide a convenient way for comparing pairs of process models with respect to their behavior or computing behavioral similarity between process models. Still, as of today, there is little understanding of the expressive power of behavioral profiles. Via counter-examples, several authors have shown that behavioral profiles over various sets of behavioral relations cannot distinguish certain systems up to trace equivalence, even for restricted classes of systems represented as safe workflow nets. This paper studies the expressive power of behavioral profiles from two angles. Firstly, the paper investigates the expressive power of behavioral profiles and systems captured as acyclic workflow nets. It is shown that for unlabeled acyclic workflow net systems, behavioral profiles over a simple set of behavioral relations are expressive up to configuration equivalence. When systems are labeled, this result does not hold for any of several previously proposed sets of behavioral relations. Secondly, the paper compares the expressive power of behavioral profiles and regular languages. It is shown that for any set of behavioral relations, behavioral profiles are strictly less expressive than regular languages, entailing that behavioral profiles cannot be used to decide trace equivalence of finite automata and thus Petri nets.

Formal security analysis of the DNP3-secure authentication protocol

This thesis evaluates the security of Supervisory Control and Data Acquisition (SCADA) systems, which are one of the key foundations of many critical infrastructures. Specifically, it examines one of the standardised SCADA protocols called the Distributed Network Protocol Version 3, which attempts to provide a security mechanism to ensure that messages transmitted between devices, are adequately secured from rogue applications. To achieve this, the thesis applies formal methods from theoretical computer science to formally analyse the correctness of the protocol.

Understanding data flow and security requirements in wireless Body Area Networks for healthcare

The Body Area Network (BAN) is an emerging technology that focuses on monitoring physiological data in, on and around the human body. BAN technology permits wearable and implanted sensors to collect vital data about the human body and transmit it to other nodes via low-energy communication. In this paper, we investigate interactions in terms of data flows between parties involved in BANs under four different scenarios targeting outdoor and indoor medical environments: hospital, home, emergency and open areas. Based on these scenarios, we identify data flow requirements between BAN elements such as sensors and control units (CUs) and parties involved in BANs such as the patient, doctors, nurses and relatives. Identified requirements are used to generate BAN data flow models. Petri Nets (PNs) are used as the formal modelling language. We check the validity of the models and compare them with the existing related work. Finally, using the models, we identify communication and security requirements based on the most common active and passive attack scenarios.

Decision support requirements for intelligent operation of southern grid in India

Control centers (CC) play a very important role in power system operation. An overall view of the system with information about all existing resources and needs is implemented through SCADA (Supervisory control and data acquisition system) and an EMS (energy management system). As advanced technologies have made their way into the utility environment, the operators are flooded with huge amount of data. The last decade has seen extensive applications of AI techniques, knowledge-based systems, Artificial Neural Networks in this area. This paper focuses on the need for development of an intelligent decision support system to assist the operator in making proper decisions. The requirements for realization of such a system are recognized for the effective operation and energy management of the southern grid in India The application of Petri nets leading to decision support system has been illustrated considering 24 bus system that is a part of southern grid.

Modelling and analysis of the variance in parallelism in parallel computations

In this paper, we introduce an analytical technique based on queueing networks and Petri nets for making a performance analysis of dataflow computations when executed on the Manchester machine. This technique is also applicable for the analysis of parallel computations on multiprocessors. We characterize the parallelism in dataflow computations through a four-parameter characterization, namely, the minimum parallelism, the maximum parallelism, the average parallelism and the variance in parallelism. We observe through detailed investigation of our analytical models that the average parallelism is a good characterization of the dataflow computations only as long as the variance in parallelism is small. However, significant difference in performance measures will result when the variance in parallelism is comparable to or higher than the average parallelism.

Stochastic modelling of flexible manufacturing systems

Mathematical modelling plays a vital role in the design, planning and operation of flexible manufacturing systems (FMSs). In this paper, attention is focused on stochastic modelling of FMSs using Markov chains, queueing networks, and stochastic Petri nets. We bring out the role of these modelling tools in FMS performance evaluation through several illustrative examples and provide a critical comparative evaluation. We also include a discussion on the modelling of deadlocks which constitute an important source of performance degradation in fully automated FMSs.

A decidable temporal logic with repeating values

Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this paper, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an infinite set is repeated in the future or in the past. Such a restriction has been inspired by a recent work on spatio-temporal logics. We show decidability of finitary and infinitary satisfiability by reduction into the verification of temporal properties in Petri nets. This is a surprising result since the logic is closed under negation, contains future-time and past-time temporal operators and can express the nonce property and its negation. These ingredients are known to lead to undecidability with a more liberal use of the freeze quantifier.

Temporal Logics of Repeating Values

Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this article, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an infinite set is repeated in the future or in the past. Such a restriction has been inspired by a recent work on spatio-temporal logics that suggests such a restricted use of the freeze operator. We show decidability of finitary and infinitary satisfiability by reduction into the verification of temporal properties in Petri nets by proposing a symbolic representation of models. This is a quite surprising result in view of the expressive power of the logic since the logic is closed under negation, contains future-time and past-time temporal operators and can express the nonce property and its negation. These ingredients are known to lead to undecidability with a more liberal use of the freeze quantifier. The article also contains developments about the relationships between temporal logics with the freeze operator and counter automata as well as reductions into first-order logics over data words.

Sistema konkurrenteak simulatzeko kernel bat: multiprozesadore sistemak

Jarraian, hainbat hilabetetan zehar garatutako proiektuaren deskribapena biltzen duen memoria dugu eskuragarri. Proiektu hau, sistema konkurrenteen simulazioan zentratzen da eta horretarako, mota honetako sistemen arloan hain erabiliak diren Petri Sareak lantzeaz gain, simulatzaile bat programatzeko informazio nahikoa ere barneratzen ditu. Gertaera diskretuko simulatzaile estatistiko batean oinarrituko da proiektuaren garapena, helburua izanik Petri Sareen bidez formalizatzen diren sistemak simulatzeko softwarea osatzea. Proiektuaren helburua da objektuetara zuzendutako hizkuntzaren bidez, Java hizkuntzaren bidez alegia, simulatzailearen programazioa erraztea eta ingurune honen baliabideak erabiltzea, bereziki XML teknologiari lotutakoak. Proiektu hau, bi zati nagusitan banatzen dela esan daiteke. Lehenengo zatiari dagokionez, konputazio munduan simulazioa aurkeztu eta honi buruzko behar adina informazio emango da. Hau, oso erabilgarria izango da programatuko den simulatzailearen nondik norakoak ulertu eta klase desberdinen inplementazioa egin ahal izateko. Horrez gain, zorizko aldagaiak eta hauen simulazioa ere islatzen dira, simulazio prozesu hori ahalik eta era errealean gauzatzeko helburuarekin. Ondoren, Petri Sareak aurkeztuko dira, hauen ezaugarri eta sailkapen desberdinak goraipatuz. Gainera, Petri Sareak definitzeko XML lengoaia erabiliko denez, mota honetako dokumentu eta eskemak aztertuko dira, hauek, garatuko den aplikazioaren oinarri izango direlarik. Bestalde, aplikazioaren muin izango diren klaseen diseinu eta inplementazioak bildu dira azken aurreko kapituluan. Alde batetik, erabili den DOM egituraren inguruko informazioa islatzen da eta bestetik, XML-tik habiatuz lortuko diren PetriNet instantziak maneiatzeko ezinbestekoak diren Java klaseen kodeak erakusten dira. Amaitzeko, egileak ateratako ondorioez gain, proiektuaren garapen prozesuan erabili den bibliografiaren berri ere ematen da.

Trace theory

The concept of traces has been introduced for describing non-sequential behaviour of concurrent systems via its sequential observations. Traces represent concurrent processes in the same way as strings represent sequential ones. The theory of traces can be used as a tool for reasoning about nets and it is hoped that applying this theory one can get a calculus of the concurrent processes anologous to that available for sequential systems. The following topics will be discussed: algebraic properties of traces, trace models of some concurrency phenomena, fixed-point calculus for finding the behaviour of nets, modularity, and some applications of the presented theory.

基于PMAC开放式数控系统软件开发

基于PC和多轴运动控制器的开放式数控系统是理想的开放式数控系统。介绍了基于PMAC的开放式数控系统结构形式,PMAC的差补、位置控制、伺服功能、以PMAC和PC机为硬件平台搭建了数控系统,并对其硬件构成和软件设计结构进行了分析。着重从软件设计的角度,介绍了PTALK控件的功能和作用,对数控系统软件构成进行了详细的阐述。并设计出了友好的用户界面,在实际应用中具有重要意义。

Guest Editorial. Special Issue: Temporal logic in engineering

Logic-based models are thriving within artificial intelligence. A great number of new logics have been defined, and their theory investigated. Epistemic logics introduce modal operators for knowledge or belief; deontic logics are about norms, and introduce operators of deontic necessity and possibility (i.e., obligation or prohibition). And then we have a much investigated class—temporal logics—to whose application to engineering this special issue is devoted. This kind of formalism deserves increased widespread recognition and application in engineering, a domain where other kinds of temporal models (e.g., Petri nets) are by now a fairly standard part of the modelling toolbox.

A mission control system for an autonomous underwater vehicle

The presented work focuses on the theoretical and practical aspects concerning the design and development of a formal method to build a mission control system for autonomous underwater vehicles bringing systematic design principles for the formal description of missions using Petri nets. The proposed methodology compounds Petri net building blocks within it to de_ne a mission plan for which it is proved that formal properties, such as reachability and reusability, hold as long as these same properties are also guaranteed by each Petri net building block. To simplify the de_nition of these Petri net blocks as well as their composition, a high level language called Mission Control Language has been developed. Moreover, a methodology to ensure coordination constraints for teams of multiple robots as well as the de_nition of an interface between the proposed system and an on-board planner able to plan/replan sequences of prede_ned mission plans is included as well. Results of experiments with several real underwater vehicles and simulations involving an autonomous surface craft and an autonomous underwater vehicles are presented to show the system's capabilities.

The SAFEE on-board threat detection system

Under the framework of the European Union Funded SAFEE project(1), this paper gives an overview of a novel monitoring and scene analysis system developed for use onboard aircraft in spatially constrained environments. The techniques discussed herein aim to warn on-board crew about pre-determined indicators of threat intent (such as running or shouting in the cabin), as elicited from industry and security experts. The subject matter experts believe that activities such as these are strong indicators of the beginnings of undesirable chains of events or scenarios, which should not be allowed to develop aboard aircraft. This project aimes to detect these scenarios and provide advice to the crew. These events may involve unruly passengers or be indicative of the precursors to terrorist threats. With a state of the art tracking system using homography intersections of motion images, and probability based Petri nets for scene understanding, the SAFEE behavioural analysis system automatically assesses the output from multiple intelligent sensors, and creates. recommendations that are presented to the crew using an integrated airborn user interface. Evaluation of the system is conducted within a full size aircraft mockup, and experimental results are presented, showing that the SAFEE system is well suited to monitoring people in confined environments, and that meaningful and instructive output regarding human actions can be derived from the sensor network within the cabin.

A grouped P2P network for scalable grid information services

Information services play a crucial role in grid environments in that the state information can be used to facilitate the discovery of resources and the services available to meet user requirements, and also to help tune the performance of a grid system. However, the large size and dynamic nature of the grid brings forth a number of challenges for information services. This paper presents PIndex, a grouped peer-to-peer network that can be used for scalable grid information services. PIndex builds on Globus MDS4, but introduces peer groups to dynamically split the large grid information search space into many small sections to enhance its scalability and resilience. PIndex is subsequently modeled with Colored Petri Nets for performance evaluation. The simulation results show that PIndex is scalable and resilient in dealing with a large number of peer nodes.