Narrow Results

Asynchronous and Synchronous languages have been in use for the specification of reactive systems. One of the main distinguishing features of these two classes lies in the way nondeterminism is used for the specification of programs. From this viewpoint, we analyze CSP (a typical asynchronous language) and ESTEREL (a synchronous language). The synchronous language Esterel is based on the notions of determinism, input nondeterminacy and parallelism whereas CSP is built on the notions of nondeterminism, concurrency and distribution. The main objectives of the study are to assess:

• The role of nondeterminism in the specification of the behaviour and realization of programs: A clear distinction between local and global nondeterminism enables us to distinguish between implementational nondeterminism and environmental/input nondeterminism. The results in this direction would enable one to achieve observable determinism where the implementational choices can be hidden and thus, analyze the program behaviour with reference to the real environmental nondeterminism in the specification. This leads to a proper refinement of specifications and aids in deriving distributed implementations of finite state transition systems that are not necessarily deterministic.

• The implementability of asynchronous languages through synchronous languages. The implementability of asynchronous languages in synchronous languages not only provides a realistic implementation but also provides higher level abstractions (such as multi-process interactions) for reactive specifications using features such as broadcast, interrupts, exception handling mechanisms etc.

In this work we present an algorithm for solving the reachability problem in finite systems that are modelled with process algebras. Our method is based on Static Analysis, in particular, Data Flow Analysis, of the syntax of a process algebraic system with multi-way synchronisation. The results of the Data Flow Analysis are used in order to build a set of Horn clauses whose least model corresponds to an overapproximation of the reachable states. The computed model can be refined after each transition, and the algorithm runs until either a state whose reachability should be checked is encountered or it is not in the least model for all constructed states and thus is definitely unreachable. The advantages of the algorithm are that in many cases only a part of the Labelled Transition System will be built which leads to lower time and memory consumption. Also, it is not necessary to save all the encountered states which leads to further reduction of the memory requirements of the algorithm.

In this paper we develop a theory for timed systems which relate to time granularity. We use the well known equivalence of bisimulation to study the effect of changing granularity. We identify situations where measuring time more accurately has no effect on the equivalence. Similarly we also present a few situations where measuring time less accurately has no effect on the equivalence. We also present properties of the situations where the semantics is indeed altered by a change in time granularity.

With the process of non-functional properties research on real-time systems, multi-resource estimation and analysis of real-time systems become a hotspot. Process algebra is a formal method that is fit for analyzing the functional properties of real-time systems, but it cannot analyze the multi-resource properties. Resource timed process algebra (RTPA) proposed in this paper can handle it efficiently by extending multi-resource semantics on timed communicating sequential process (TCSP). The multi-resource consumption of real-time instruction is mapped into the resource vector of RTPA, and then the multi-resource consumption of real-time systems can be modeled and optimized by using RTPA; the resource optimal checking algorithms are proposed to check the multi-resource satisfiability of instructions and calculate the minimum resource and accumulated resource of real-time systems. This formal method improves the accuracy and efficiency of multi-resource calculation, and the calculation results can be further used to quantitatively analyze and optimize the multi-resource consumption of real-time systems.

Probabilistic behavior is omnipresent in computer-controlled systems, in particular, so-called safety-critical hybrid systems, due to various reasons, like uncertain environments or fundamental properties of nature. In this paper, we extend the existing hybrid process algebra ACP${}_{hs}^{srt}$ with probability without sacrificing the nondeterministic choice operator. The existing approximate probabilistic bisimulation relation is fragile and not robust in the sense of being dependent on the deviation range of the transition probability. To overcome this defect, a novel approximate probabilistic bisimulation is proposed which is inspired by the idea of Probably Approximately Correct (PAC) by relaxing the constraints of transition probability deviation range. Traditional temporal logics, even probabilistic temporal logics, are expressive enough, but they are limited to producing only true or false responses, as they are still logics and not suitable for performance evaluation. To settle this problem, we present a new performance evaluation language that expands quantitative analysis from the value range of $\{0,1\}$ to real number to reason over probabilistic systems. After that, the corresponding algorithms for performance evaluation are given. Finally, an industrial example is given to demonstrate the effectiveness of our method.

Cyber-Physical Systems (CPS) are the next generation of intelligent systems that integrate information control devices with physical resources. With increasingly close connections between CPS components and frequent interactions, potential defects grow exponentially, rendering the operating environment of CPS unreliable. Therefore, research on methods and theories to ensure the correctness, safety and reliability of CPS is not only an important research topic but also an inevitable challenge. In this paper, we propose a CPS modeling and verification method based on Architecture Analysis & Design Language (AADL) and process algebra to address this challenge. Due to the continuous, time-constrained, stochastic, uncertain and concurrent characteristics of CPS, this paper considers both flexibility and rigor in the modeling process. We first extend the ability of AADL to describe the multiple characteristics of CPS and propose Hybrid Probability-AADL (HP-AADL). Second, this paper introduces conditional execution, conditional interruption and probability operators into Temporal Calculus of Communication Systems (TCCS) and designs a new formal modeling language Hybrid Probability-Temporal Calculus of Communication Systems (HP-TCCS). However, HP-AADL is a semi-formal modeling language that cannot be directly used for formal verification, it cannot strictly guarantee the quality of the established CPS models, including its functional correctness and safety. Therefore, this paper proposes transformation rules from HP-AADL to HP-TCCS, which enables model checking of CPS models described in HP-AADL within HP-TCCS. Additionally, this paper designs a new formal specification language HPAT-Spatial Temporal Logic (HPAT-STL) based on Probabilistic Computation Tree Logic (PCTL) and Spatial Logic, which characterizes the temporal, probabilistic and spatial properties of CPS model. To achieve formal verification of HP-TCCS model and HPAT-STL formulas, this paper proposes a model checking algorithm HPAT-Model Checking Algorithm (HPAT-MCA). Finally, we discuss a typical CPS example to demonstrate the effectiveness of our proposed method in ensuring correct, safe and reliable CPS.

Aiming at the shortcomings of the modeling analysis of traditional Feature-Oriented Analysis Approach under service oriented architecture SOA, and providing more reusability and flexibility to the development of SOA system, this paper makes an improvement on Feature-Oriented Analysis Approach. It introduces the concept of service feature and improves the refinement and interaction description of feature models. On the basis of this, it proposes a method of domain analysis in SOA. In addition, in view of the fact that web services act as a technology available to implement SOA, it presents a method to transform feature model into interface model and composite model of web services. Finally, this method's application in ERP system project in publishing is verified as an example to show that it is feasible to improve software development efficiency.

Based on the concept of DNA strand displacement and DNA strand algebra we have developed a method for logical inference which is not based on silicon-based computing. Essentially, it is a paradigm shift from silicon to carbon. In this paper, we have considered the inference mechanism, viz. modus ponens, to draw conclusion from any observed fact. Thus, the present approach to logical inference based on DNA strand algebra is basically an attempt to develop expert system design in the domain of DNA computing. We have illustrated our methodology with respect to the worked out example. Our methodology is very flexible for implementation of different expert system applications.

For process algebra as a major branch of abstract description languages, almost no work directly exploits the structural symmetry in it. In this paper, a process is defined as an algebraic structure. We define a notion of symmetry for processes based on permutation groups. Given a process and a permutation group over it, we give the quotient process of this process and show that the quotient process is bisimulation equivalent to the original process. Moreover, we present the algorithm for this structural reduction.

Correctness of a system depends on the correct execution of transactions. For large systems, e.g., web-based, these transactions involve more than one component and hence more than one independent entity. Such transactions are called Long Running Transaction(LRT) as they coordinate complex interactions among multiple sub-systems. Well known roll-back mechanism do not suffice to handle faults in LRTs, therefore compensation mechanisms are introduced. However, introduced structures are complex and hard to understand and handle. Formal methods are well known tool for modelling, analysis and synthesis of complex systems. In this chapter we present a technique that allows modelling LRTs using Compensating CSP, then translating them to Promela language and analyzing using SPIN tool. We have modelled and verified the LRTs. We exemplify it using a web service called Air-ticket Reservation System (ATRS).

In this study, we propose a formal approach for the analysis of robustness with regard to human-made faults in procedural manuals. In many cases, fault detection and recovery tasks are embedded in procedural manuals that allow us to detect human-made faults. This investigation is important in preserving the trust of workflows in safety critical domains. We define the formal semantics of human-made faults according to Discrete Action Classification, which classifies fault actions of experts in a domain — the formal definition of the faults is based on a transition system. Using these semantics, we inject faults into a fault-free model of a procedural manual. After that, we verify that the model embedded with faulty tasks satisfies a property as the goal of a procedural manual by model checking. A model checking tool is given the opposite of the formula as a goal, and if this tool reports counter examples, we say that the procedural manual is not robust. We apply our framework to a procedural manual that a nurse executes for taking blood samples. In the case, we conclude that the procedural manual is not robust because that tool reports counter examples.