An I/O Automata-based Approach to Verify Component Compatibility: Application to the CyCab Car

An interesting formal approach to specify component interfaces is interface automata based approach, which is proposed by L. Alfaro and T. Henzinger. These formalisms have the ability to model both the input and output requirements of components system. In this paper, we propose a method to enrich interface automata by the semantics of actions in order to verify components interoperability at the levels of signatures, semantics, and protocol interactions of actions. These interfaces consist of a set of required and offered actions specified by Pre and Post conditions. The verification of the compatibility between interface automata reuse the L. Alfaro and T. Henzinger proposed algorithm and adapt it by taking into account the action semantics. Our approach is illustrated by a case study of the vehicle CyCab.     

A Contract-based Approach to Specifying and Verifying Safety Critical Systems

Light-weight formal method has been regarded as an important approach to development of component-based safety critical systems. The paper proposes an approach which can formally specify and verify the contract of static structure, dynamic behavior and refinement of component systems based on UML 2.0 superstructure. As results, the correctness of static contract can be obtained via type checking of interfaces and connectors. Dynamic contract can be verified through determining the cooperativeness of integrated components, whose contracts are depicted with interface protocol state machines and their semantics models, namely contract automata. The refinement relation between high level component and its implementation will be guaranteed through defining the alternating simulation between contract automata of components at different levels.     

Aspects of availability: Enforcing timed properties to prevent denial of service

We propose a domain-specific aspect language to prevent denial of service caused by resource management. Our aspects specify availability policies by enforcing time limits in the allocation of resources. In our language, aspects can be seen as formal timed properties on execution traces. Programs and aspects are specified as timed automata and the weaving process as an automata product. The benefit of this formal approach is two-fold: the user keeps the semantic impact of weaving under control and (s)he can use a model-checker to optimize the woven program and verify availability properties. This article presents the main approach (programs, aspects, weaving) formally using timed safety automata. The specification of resources, optimizations and verification are sketched in a more intuitive fashion. Even if a concrete implementation remains as future work, we address some high-level implementation issues and illustrate the approach by small examples and a case study.     

基于自动机的构件实时交互行为的形式化模型

采用形式化方法对复杂实时构件系统交互行为进行描述和验证,对于提高系统的正确性、可靠性等可信性质具有重要意义.分析了基于进程代数和自动机的构件交互行为形式化建模方法各自的优缺点,在此基础上提出了基于时间构件交互自动机的建模方法,给出了时间构件交互自动机的相关定义、组合和验证算法.时间构件交互自动机引入了时间限制、时间代价、时间代价计算半环、构件组合层次等概念,既能够描述构件交互情况,又能够清楚地表示出构件系统的体系结构信息和实时信息,便于对系统进行描述和验证.最后,结合具体应用给出了应用示例.     

Toward a comprehensive treatment of temporal constraints about periodic events

In this article, we propose an Allen‐like approach to deal with different types of temporal constraints about periodic events. We consider the different components of such constraints (thus, unlike Allen, we also take into account quantitative constraints) including frame times, user‐defined periods, qualitative temporal constraints, and numeric quantifiers and the interactions between such components. We propose a specialized high‐level formalism to represent temporal constraints about periodic events; temporal reasoning on the formalism is performed by a path‐consistency algorithm repeatedly applying our operations of inversion, intersection, and composition and by a specialized reasoner about periods and numeric quantification. The high‐level formalism has been designed in such a way that different types of temporal constraints about periodic events can be represented in a compact and (hopefully) user‐friendly way and path‐consistency‐based temporal reasoning on the formalism can be performed in polynomial time. We also prove that our definitions of inversion, intersection, and composition and, thus, of our path‐consistency algorithm, are correct. This article also sketches the general architecture of the temporal manager for periodic events (TeMP⁺), that has been designed on the basis of our approach. As a working example, we show an application of our approach to scheduling in a school. © 2003 Wiley Periodicals, Inc.     

接口自动机--一种用于组件组合的形式系统

接口自动机是描述基于组件系统中组件及组件间交互行为的形式化工具。接口自动机在处理组件组合问题时所使用的“乐观方法”和博弈思想是区别于其它形式化工具的关键点。本文对接口自动机、时间接口自动机和资源接口及其中的博弈思想进行综述。在同其它形式化方法比较的基础上,指出了接口自动机的长处和局限。文中总结了接口自动机在理论上和实际中的意义并对其应用前景做了展望。     

Specifying and verifying contract-driven service compositions using commitments and model checking

The paper proposes a novel model checking-based approach towards verifying the compliance of intelligent agent-based web services with contracts regulating their compositions specified in the Business Process Execution Language (BPEL). Unlike the existing approaches in the literature, the main contribution and impact of the introduced approach is the ability to verify intelligent and autonomous composite web services by capturing and describing in details both compliance and violation behaviors, how the system can distinguish between them, and how the system reacts and can be recovered after each violation. The approach encompasses three contributing parts, namely: 1) the marking process of an extended BPEL; 2) the transformation of the extended and marked BPEL to an automata model; and 3) the encoding of the resulting automata model into the Interpreted Systems Programming Language (ISPL), the input language of the MCMAS model checker for intelligent and autonomous multi-agent systems. In the first part, we extend BPEL that specifies the business process of the composition by creating custom activities called labels. We use those labels as means to represent the specifications and mark the points the developer aims to verify. A significant advantage of this labeling is the ability to highlight specific points in the design to be verified and to distinguish compliance behaviors from violations, which makes this verification focused and highly efficient. In the second part, we introduce new transformation rules to transform the extended and marked BPEL to an automata model. This transformation requires a prior modeling of agent-based web services composition using automata definitions. In the third part, we introduce algorithmic translation rules encoding the resulting automata model into ISPL. This translation makes model checking the behavior of our contract-driven compositions possible. A novel characteristic of the proposed approach is the automatic generation of the properties against which the system is verified from the composition’s implementation, which is technically challenging. The verification properties are expressed in the Computation Tree Logic of Commitments (CTLC). Technically, CTLC provides a powerful representation to formally model 1) interactions among multi-agent based web services and 2) compliance and violation behaviors within composite business contracts by making use of communicative commitment operators. CTLC also includes a fulfillment operator which helps formally check the compliance with business contracts and specify the system recovery. A detailed case study from expert and intelligent systems domain along with experimental results are also reported in the paper. Finally, the main impact and significance of the paper on expert and intelligent systems is the ability to use these systems safely since there is a way to verify if the intelligent components behave according to and in compliance with the underlying regulating contracts.     

Proving Invariants of I/O Automata with TAME

This paper describes a specialized interface to PVS called TAME (Timed Automata Modeling Environment) which provides automated support for proving properties of I/O automata. A major goal of TAME is to allow a software developer to use PVS to specify and prove properties of an I/O automaton efficiently and without first becoming a PVS expert. To accomplish this goal, TAME provides a template that the user completes to specify an I/O automaton and a set of proof steps natural for humans to use for proving properties of automata. Each proof step is implemented by a PVS strategy and possibly some auxiliary theories that support that strategy. We have used the results of two recent formal methods studies as a basis for two case studies to evaluate TAME. In the first formal methods study, Romijn used I/O automata to specify and verify memory and remote procedure call components of a concurrent system. In the second formal methods study, Devillers et al. specified a tree identify protocol (TIP), part of the IEEE 1394 bus protocol, and provided hand proofs of TIP properties. Devillers also used PVS to specify TIP and to check proofs of TIP properties. In our first case study, the third author, a new TAME user with no previous PVS experience, used TAME to create PVS specifications of the I/O automata formulated by Romijn and Devillers et al. and to check their hand proofs. In our second case study, the TAME approach to verification was compared with an alternate approach by Devillers which uses PVS directly.     

Interface theories for concurrency and data

We present a compositional approach for specifying concurrent behavior of components with data states on the basis of interface theories. The dynamic aspects of a system are specified by modal input/output automata, whereas changing data states are specified by pre- and postconditions. The combination of the two formalisms leads to our notion of modal input/output automata with data constraints (MIODs). In this setting we study refinement and behavioral compatibility of MIODs. We show that compatibility is preserved by refinement and that refinement is compositional w.r.t. synchronous composition, thus satisfying basic requirements of an interface theory. We propose a semantic foundation of interface specifications where any MIOD is equipped with a model-theoretic semantics describing the class of its correct implementation models. Implementation models are formalized in terms of guarded input/output transition systems and the correctness notion is based on a simulation relation between an MIOD and an implementation model which relates not only abstract and concrete control states but also (abstract) data constraints and concrete data states. We show that our approach is compositional in the sense that locally correct implementation models of compatible MIODs compose to globally correct implementations, thus ensuring independent implementability.     

A multicontext architecture for formalizing complex reasoning

We propose multicontext systems (MC systems) as a formal framework for the specification of complex reasoning. MC systems provide the ability to structure the specification of “global” reasoning in terms of “local” reasoning subpatterns. Each subpattern is modeled as a deduction in a context, formally defined as an axiomatic formal system. the global reasoning pattern is modeled as a concatenation of contextual deductions via bridge rules, i.e., inference rules that infer a fact in one context from facts asserted in other contexts. Besides the formal framework, in this article we propose a three-layer architecture designed to specify and automatize complex reasoning. At the first level we have object-level contexts (called s-contexts) for domain specifications. Problem-solving principles and, more in general, meta-level knowledge about the application domain is specified in a distinct context, called Problem-Solving Context (PSC). On top of s-contexts and PSC, we have a further context, called MT, where it is possible to specify strategies to control multicontext reasoning spanning through s-contexts and PSC. We show how GETFOL can be used as a computer tool for the implementation of MC systems and for the automatization of multicontext deductions. © 1995 John Wiley & Sons, Inc.     

Graphic modeling in Distributed Autonomous and Asynchronous Automata (DA3)

Automated verification of distributed systems becomes very important in distributed computing. The graphical insight into the system in the early and late stages of the project is essential. In the design phase, the visual input helps to articulate the collaborative distributed components clearly. The formal verification gives evidence of correctness or malfunction, but in the latter case, graphical simulation of counterexample helps for better understanding design errors. For these purposes, we invented Distributed Autonomous and Asynchronous Automata (DA³), which have the same semantics as the formal verification base—Integrated Model of Distributed Systems (IMDS). The IMDS model reflects the natural characteristics of distributed systems: unicasting, locality, autonomy, and asynchrony. Distributed automata have all of these features because they share the same semantics as IMDS. In formalism, the unified system definition has two views: the server view of the cooperating distributed nodes and the agent view of the migrating agents performing distributed computations. The automata have two formally equivalent forms that reflect two views: Server DA³ for observing servers exchanging messages, and Agent DA³ for tracking agents, which visit individual servers in their progress of distributed calculations. We present the DA³ formulation based on the IMDS formalism and their application to design and verify distributed systems in the Dedan environment. DA³ formalism is compared with other concepts of distributed automata known from the literature.

     

支持扩展虚拟同步的组通信算法形式描述与验证

组通信系统是为方便开发容错的分布式应用系统而提出的一种通信中间件．虚拟同步是组通信系统中的一个重要概念．其本质是限制向所有组成员递交组成员资格变化信息和应用消息的次序．为支持网络可划分的情况，引入了扩展虚拟同步模型．针对扩展虚拟同步模型的特点，提出了一种基于客户／服务器模式的组通信系统架构，并以I／O自动机的形式给出系统内部各模块的服务和算法．最后以继承建模的方式逐步给出该算法的自动机模型，并用形式化的方法验证其正确性．     

Concurrent Logic and Automata Combined: A Semantics for Components

In this paper, we describe a true-concurrent hierarchical logic interpreted over concurrent automata. Concurrent automata constitute a special kind of asynchronous transition system (ATS) used for modelling the behaviour of components as understood in component-based software development. Here, a component-based system consists of several interacting components whereby each component manages calls to and from the component using ports to ensure encapsulation. Further, a component can be complex and made of several simpler interacting components. When a complex component receives a request through one of its ports, the port delegates the request to an internal component. Our logic allows us to describe the different views we can have on the system. For example, the overall component interactions, whether they occur sequentially, simultaneously or in parallel, and how each component internally manages the received requests (possibly expressed at different levels of detail). Using concurrent automata as an underlying formalism we guarantee that the expressiveness of the logic is preserved in the model. In future work, we plan to integrate our truly-concurrent approach into the Edinburgh Concurrency Workbench.     

A Supervisory Control Method for Ensuring the Conformance of Real-Time Discrete Event Systems

In this article, we study the problem of controlling a plant described as a real-time discrete event system. The aimed objective is to ensure a conformance relation denoted tioco between the plant and the formal specification of the system, by means of a supervisor. We adopt a two-step approach. In Step 1, we express the problem into a non-real-time form, by using a transformation of timed automata (TA) into particular finite state automata called Set-Exp-Automata (SEA). The latter use two additional types of events, Set and Exp. And in Step 2, we propose a non-real-time control method suitable for SEA. We also propose a control architecture.     

网构软件的随机性资源自适应性的形式化分析与验证

因特网上的资源具有不确定性、随机性,需要考虑如何保证网构软件系统在运行中满足资源需求。使用随机性资源接口自动机对软件构件的行为进行形式化建模,并使用随机性资源接口自动机网络描述构件组装系统的组合行为;在资源不确定的情况下,检验组合系统是否满足资源约束,并提出基于可达图的相应算法。给出了一个实例网上书店系统,并用模型检测工具Spin验证了模型的正确性。     

Timed Semantics of Message Sequence Charts Based on Timed Automata

Message Sequence Charts (MSCs) provide a way for quick and easily understandable modelling of concurrent systems. Apart from their intuitive semantics easily deduced from their visual syntax, there is a formally defined semantics—Unfortunately, the semantics intuitively assigned to them is sometimes at odds with the formal semantics. In this paper, we will show an alternative approach to the semantics of MSCs, which will enable us to formally model their timed behaviour. Furthermore, we show how some generalizations of ordering events can lead to a language better suited to model real-world requirements. To ease the task of analyzing (High-Level) MSCs, we identify a subclass of those which can be translated into finite (timed of untimed) automata and specify the translation, thus laying the foundation for model checking.     

A new formalism for mathematical description and verification of component-based systems

In this paper, we introduce a formal approach for composing software components into a distributed system. We describe the system as a hierarchical composition of some components, which can be distributed on a wide variety of hardware platforms and executed in parallel. We represent each component by a mathematical model and specify the abstract communication protocols of the components using Interface Automata (IAs). To model hierarchical systems, besides the basic components’ model, we will present other components, called nodes. A node consists of a set of subnodes interacting under the supervision of a controller. Each subnode, in turn, is a node or discrete event component. By considering a subnode as a node we can make hierarchical nodes/components. The entire system, therefore, forms the root of the hierarchy. A controller, in turn, is a set of subcontrollers/interface automata that specifies interaction protocol of the components inside a node. We have also presented an example demonstrating the model by illustrating nodes, subnodes, controllers, and subcontrollers. To address the state space explosion problem in system verification, we utilize the controller as a contract for independent analysis of the components and their interactions. Therefore, a node will not be analyzed directly; instead, we will analyze the controller.     

Specifying and checking method call sequences of Java programs

In a pre and postcondition-style specification, it is difficult to specify the allowed sequences of method calls, referred to as protocols. The protocols are essential properties of reusable object-oriented classes and application frameworks, and the approaches based on the pre and postconditions, such as design by contracts (DBC) and formal behavioral interface specification languages (BISL), are being accepted as a practical and effective tool for describing precise interfaces of (reusable) program modules. We propose a simple extension to the Java Modeling Language (JML), a BISL for Java, to specify protocol properties in an intuitive and concise manner. The key idea of our approach is to separate protocol properties from functional properties written in pre and post-conditions and to specify them in a regular expression-like notation. The semantics of our extension is formally defined and provides a foundation for implementing runtime checks. Case studies have been performed to show the effectiveness our approach. We believe that our approach can be adopted by other BISLs.