Executable specifications for embedded distributed systems

Combining hardware components with an executable specification language facilitates the specification prototyping of embedded distributed systems. The specification language should cover process management, timing, and communication commands that real-time executive and communication task services of every node prototype can interpret. We use a technique that employs attribute grammars and either a macro processor or Prolog to execute the language     

On the refinement of liveness properties of distributed systems

We present a new approach, based on simulation relations, for reasoning about liveness properties of distributed systems. Our contribution consists of (1) a formalism for defining liveness properties, (2) a proof method for liveness properties based on that formalism, and (3) two expressive completeness results: our formalism can express any liveness property which satisfies a natural “robustness” condition; and also any liveness property at all, provided that history variables can be used. To define liveness, we generalize complemented-pairs (Streett) automata to an infinite state-space, and an infinite number of complemented-pairs. Our proof method provides two techniques: one for refining liveness properties across levels of abstraction, and another for refining liveness properties within a level of abstraction. The first is based on extending simulation relations so that they relate the liveness properties of an abstract automaton to those of a concrete automaton. The second is based on a deductive method for inferring new liveness properties of an automaton from already established liveness properties of the same automaton. This deductive method is diagrammatic, and is based on constructing “lattices” of liveness properties.     

Verifying distributed real-time properties of embedded systems via graph transformations and model checking

Component middleware provides dependable and efficient platforms that support key functional, and quality of service (QoS) needs of distributed real-time embedded (DRE) systems. Component middleware, however, also introduces challenges for DRE system developers, such as evaluating the predictability of DRE system behavior, and choosing the right design alternatives before committing to a specific platform or platform configuration. Model-based technologies help address these issues by enabling design-time analysis, and providing the means to automate the development, deployment, configuration, and integration of component-based DRE systems. To this end, this paper applies model checking techniques to DRE design models using model transformations to verify key QoS properties of component-based DRE systems developed using Real-time CORBA. We introduce a formal semantic domain for a general class of DRE systems that enables the verification of distributed non-preemptive real-time scheduling. Our results show that model-based techniques enable design-time analysis of timed properties and can be applied to effectively predict, simulate, and verify the event-driven behavior of component-based DRE systems. This research was supported by the NSF Grants CCR-0225610 and ACI-0204028 Gabor Madl is a Ph.D. student and a graduate student researcher at the Center for Embedded Computer Systems at the University of California, Irvine. His advisor is Nikil Dutt. His research interests include the formal verification, optimization, component-based composition, and QoS management of distributed real-time embedded systems. He received his M.S. in computer science from Vanderbilt University and in computer engineering from the Budapest University of Technology and Economics. Dr. Sherif Abdelwahed received his Ph.D. degree in Electrical and Computer Engineering from the University of Toronto, Canada, in 2001. During 2000–2001, he was a research scientist with the system diagnosis group at the Rockwell Scientific Company. Since 2001 he has been with the Department of Electrical Engineering and Computer Science at Vanderbilt University as a Research Assistant Professor. His research interests include verification and control of distributed real-time systems, and model-based diagnosis of discrete-event and hybrid systems. Dr. Douglas C. Schmidt is a Professor of Computer Science, Associate Chair of the Computer Science and Engineering program, and a Senior Researcher in the Institute for Software Integrated Systems (ISIS) all at Vanderbilt University. He has published over 300 technical papers and 6 books that cover a range of research topics, including patterns, optimization techniques, and empirical analyses of software frameworks and domain-specific modeling environments that facilitate the development of distributed real-time and embedded (DRE) middleware and applications. Dr. Schmidt has served as a Deputy Office Director and a Program Manager at DARPA, where he lead the national R&D effort on middleware for DRE systems. In addition to his academic research and government service, Dr. Schmidt has over fifteen years of experience leading the development of ACE, TAO, CIAO, and CoSMIC, which are widely used, open-source DRE middleware frameworks and model-driven tools that contain a rich set of components and domain-specific languages that implement patterns and product-line architectures for high-performance DRE systems.     

Data refinement of mixed specifications

Using predicate transformers as a basis, we give semantics and refinement rules for mixed specifications that allow UNITY style specifications to be written as a combination of abstract program and temporal properties. From the point of view of the programmer, mixed specifications may be considered a generalization of the UNITY specification notation to allow safety properties to be specified by abstract programs in addition to temporal properties. Alternatively, mixed specifications may be viewed as a generalization of the UNITY programming notation to allow arbitrary safety and progress properties in a generalized ‘always section’. The UNITY substitution axiom is handled in a novel way by replacing it with a refinement rule. The predicate transformers foundation allows known techniques for algorithmic and data-refinement for weakest precondition based programming to be applied to both safety and progress properties. In this paper, we define the predicate transformer based specifications, specialize the refinement techniques to them, demonstrate soundness, and illustrate the approach with a substantial example. Received: 1 April 1996 / 6 March 1997     

Executable formal specifications of complex distributed systems with CoreASM

Formal specifications play a crucial role in the design of reliable complex software systems. Executable formal specifications allow the designer to attain early validation and verification of design using static analysis techniques and accurate simulation of the runtime behavior of the system-to-be. With increasing complexity of software-intensive computer-based systems and the challenges of validation and verification of abstract software models prior to coding, the need for interactive software tools supporting executable formal specifications is even more evident. In this paper, we discuss how CoreASM, an environment for writing and running executable specifications according to the ASM method, provides flexibility and manages the complexity by using an innovative extensible language architecture.     

Graph transformations for object-oriented refinement

An object-oriented program consists of a section of class declarations and a main method. The class declaration section represents the structure of an object-oriented program, that is the data, the classes and relations among them. The execution of the main method realizes the application by invoking methods of objects of the classes defined in the class declarations. Class declarations define the general properties of objects and how they collaborate with each other in realizing the application task programmed as the main method. Note that for one class declaration section, different main methods can be programmed for different applications, and this is an important feature of reuse in object-oriented programming. On the other hand, different class declaration sections may support the same applications, but these different class declaration sections can make significant difference with regards to understanding, reuse and maintainability of the applications. With a UML-like modeling language, the class declaration section of a program is represented as a class diagram, and the instances of the class diagram are represented by object diagrams, that form the state space of the program. In this paper, we define a class diagram and its object diagrams as directed labeled graphs, and investigate what changes in the class structure maintain the capability of providing functionalities (or services). We formalize such a structure change by the notion of structure refinement. A structure refinement is a transformation from one graph to another that preserves the capability of providing services, that is, the resulting class graph should be able to provide at least as many, and as good, services (in terms of functional refinement) as the original graph. We then develop a calculus of object-oriented refinement, as an extension to the classical theory of data refinement, in which the refinement rules are classified into four categories according to their natures and uses in object-oriented software design. The soundness of the calculus is proved and the completeness of the refinement rules of each category is established with regard to normal forms defined for object-oriented programs. These completeness results show the power of the simple refinement rules. The normal forms and the completeness results together capture the essence of polymorphism, dynamic method binding and object sharing by references in object-oriented computation.     

A tactic language for refinement of state-rich concurrent specifications

Circus is a refinement language in which specifications define both data and behavioural aspects of concurrent systems using a combination of Z and CSP. Its refinement theory and calculus are distinctive, but since refinements may be long and repetitive, the practical application of this technique can be hard. Useful strategies have been identified, described, and used, and by documenting them as tactics, they can be expressed and repeatedly applied as single transformation rules. Here, we present ArcAngelC, a language for defining such tactics; we present the language, its semantics, and its application in the formalisation of an existing strategy for verification of Ada implementations of control systems specified by Simulink diagrams. We also discuss its mechanisation in a theorem prover, ProofPower-Z.     

Automating data conversion for heterogeneous distributed shared memory

This paper describes the issues involved in sharing data among processes executing co-operatively in a heterogeneous computing environment. In a heterogeneous environment, the physical representation of a data object may need to be transformed when the object is moved from one type of processor to another. As a part of a larger project to build a heterogeneous distributed shared memory system we developed an automated tool for generating the conversion routines that are used to implement representation conversion for data objects. We developed a novel method for processing source programs that allowed us to extract detailed information about the physical representation of data objects without access to the source code of the compilers that were generating those representations. A performance comparison with the more general XDR heterogeneous data conversion package shows that the customized conversion routines that we generate are 4 to 8 times faster.     

Control synthesis via state feedback with finite frequency specifications for time-delay systems

This article considers the problem of control synthesis via state feedback for linear time-delay systems with design specifications in finite frequency ranges. First, a finite frequency performance analysis condition for time-delay systems is presented. Then, a resulting state feedback control synthesis condition is given in terms of solutions to a set of linear matrix inequalities (LMIs). Finally, the design procedure and the effectiveness of the proposed method are illustrated via a numerical design example.     

A refinement calculus for specifications in Hennessy-Milner logic with recursion

This paper is about specification and verification of processes, modelled as CCS-agents. We show, by means of examples that Hennessy-Milner Logic (HML) with recursion is a suitable language for expressing implicit or partial specifications. By extending this specification language withrefinement operators, i.e. operators that describe the internal structure of a system, we obtain a calculus for stepwise refinement of agents from a specification in HML to a realisation in CCS. The method is demonstrated by proving the alternating-bit protocol under weak assumptions about the unreliable media.This paper has also be presented at the BCS-FACS workshop on Specification and Verification of Concurrent Systems, University of Stirling, July 1988, under the title: Hennessy-Milner logic with recursion as a specification language, and a refinement calculus based on it.     

分布式系统中基于迷乱变换的代码保护方案

总结了软件迷乱技术的发展现状,提出一种在分布式环境下利用并发进程的局部状态构造分布式不透明分支、利用进程间的通信模式改变局部状态以增强迷乱强度的代码保护方案,对现有的分布式代码迷乱算法做了一定的改进,并对该方案做了性能分析。     

Practical synthesis of reactive systems from LTL specifications via parity games

Acta Informatica - The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption...     

Robust cooperative control for multi-agent systems via distributed output regulation

Robust cooperative control for multi-agent systems is considered in this paper, under the framework of the distributed output regulation problem. With some fundamental assumptions, two necessary and sufficient conditions are given for the distributed output regulation problem to be solvable. The algorithm of designing the robust distributed control law is provided, with the help of internal models. It is shown that this robust controller is effective in a neighborhood of the nominal system, which is tolerant of system uncertainties.     

Coupling-based transformations of Z specifications into UML diagrams

Due to their accuracy in describing systems, formal specifications can play an important role during forward as well as reverse engineering activities. However, besides dense mathematical expressions, their lack in visually appealing notations impedes their use and exchange among different stakeholders. One solution to this problem is to enrich the specification by other views, in most cases Unified Modelling Language (UML) diagrams. But the mapping is not trivial, and existing approaches have their impediments, among them the assignment of methods to classes—which has to be re-done by hand quite often. By the example of Z, this paper demonstrates that the situation can be improved. The new approach combines existing mapping strategies, but additionally lets the assignment of methods rest on quality-related measures. The basic idea is to balance the values of coupling for all methods within and between the UML classes. With that, two issues are addressed: firstly, the mapping of sets, types, and operations (to UML classes and UML methods) is based on reproducible measures that are intuitively comprehensible. Secondly, implementations based on the resulting UML class diagrams very likely also have comparable quality-related properties.     

Isomorphic transformations of uncertainties for incorporating EMYCIN-style and PROSPECTOR-style systems into a distributed expert system

In the past,expert systems exploited mainly the EMYCIN model and the PROSPECTOR mdoel to deal with uncertaintes.In other words,a lot of stand-alone expert systems which use thse two models are available.If we can use the Internet to Couple them together,their performance will be improved through cooperation.This is because the problem-solving ability of expert systems is greatly improved by the way of cooperation among different expert systems in a distributed expert system.Cooperation between different expert systems with these two heterogeneous uncertain reasoning models is essentially based on the transformations of uncertainties of propositions between these two models.In this paper,we discovered the exactly isomorphic transformations uncertaintis between uncertain reasoning models,as used by EMYCIN and PROSPECTOR.     

Reconfigurability of behavioural specifications for manufacturing systems

Reconfigurable manufacturing systems (RMS) support flexibility in the product variety and the configuration of the manufacturing system itself in order to enable quick adjustments to new products and production requirements. As a consequence, an essential feature of RMS is their ability to rapidly modify the control strategy during run-time. In this paper, the particular problem of changing the specified operation of a RMS, whose logical behaviour is modelled as a finite state automaton, is addressed. The notion of reconfigurability of specifications (RoS) is introduced and it is shown that the stated reconfiguration problem can be formulated as a controlled language convergence problem. In addition, algorithms for the verification of RoS and the construction of a reconfiguration supervisor are proposed. The supervisor is realised in a modular way which facilitates the extension by new configurations. Finally, it is shown that a supremal nonblocking and controllable strict subautomaton of the plant automaton that fulfils RoS exists in case RoS is violated for the plant automaton itself and an algorithm for the computation of this strict subautomaton is presented. The developed concepts and results are illustrated by a manufacturing cell example.     

Hierarchical optimal control for distributed parameter systems via block pulse operator

This paper presents a development of the hierarchical optimal control for distributed parameter systems via block pulse operator. The proposed algorithm enables one to solve optimal control of distributed parameter systems with hierarchical structure and as a result, the resulting solutions are piecewise constant with minimal mean-square error, The algorithm is simple in form and computationally advantageous. An illustrative example shows the applicability of the proposed method in practice.     

Asymptotic regulation for distributed parameter systems via zero dynamics inverse design

In this paper, we introduce a new approach, zero dynamics inverse (ZDI) design, for designing a feedback compensation scheme achieving asymptotic regulation for a linear or nonlinear distributed parameter system in the case when the value w(t) at time t of the signal w to be tracked or rejected is a measured variable. Following the nonequilibrium formulation of output regulation, we formulate the problem of asymptotic regulation by requiring zero steady‐state error together with ultimate boundedness of the state of the system and the controller(s), with a bound determined by bounds on the norms of the initial data and w. Because a controller solving this problem depends only on a bound on the norm of w not on the particular choice of w, this formulation is in sharp contrast to both exact tracking, asymptotic tracking or dynamic inversion of a completely known trajectory and to output regulation with a known exosystem. The ZDI design consists of the interconnection, via a memoryless filter, of a stabilizing feedback compensator and a cascade controller, designed in a simple, universal way from the zero dynamics of the closed‐loop feedback system. This design philosophy is illustrated with a problem of asymptotic regulation for a boundary controlled viscous Burgers' equation, for which we prove that the ZDI is input‐to‐state stable. In infinite dimensions, however, input‐to‐state stable compactness arguments are supplanted by smoothing arguments to accommodate crucial technical details, including the global existence, uniqueness, and regularity of solutions to the interconnected systems. Copyright © 2011 John Wiley & Sons, Ltd.