Integral: Petri-net approach to distributed software development

As the architecture of modern software systems continues to evolve in a distributed fashion, the development of such systems becomes increasingly complex, which requires the integration of more sophisticated specification techniques, tools, and procedures into the conventional methodology. An essential capability of an integrated software development environment is a formal specification method to capture effectively the system's functional requirements as well as its performance requirements. A validation and verification (V&V) system based on a formal specification method is of paramount importance to the development and maintenance of distributed systems.

There has been recent interest in integrating software techniques and tools at the specification level. It is also noted that an effective way of achieving such integration is by using wide-spectrum specification techniques. In view of these points, an integrated V&V system, called Integral, is presented that provides comprehensive and homogeneous analysis capabilities to both specification and testing phases of the life-cycle of distributed software systems. The underlying software model that supports various V&V activities in Integral is primarily based on Petri nets and is intended to be wide spectrum. The ultimate goal of this research is to demonstrate to the software industry, domestic or foreign, the availability and applicability of a new Petri-net-based software development paradigm. Integral is a prototype V&V system to support such a paradigm.     

Formal verification of dependable distributed protocols

Dependable distributed systems often employ a hierarchy of protocols to provide timely and reliable services. Such protocols have both dependability and real-time attributes, and the verification of such composite services is a problem of growing complexity even when using formal approaches. Our intention in this paper is to exploit the modular design aspects appearing in most dependable distributed protocols to provide formal level of assurance for their correctness. We highlight the capability of our approach through a case study in formal modular specification and tool-assisted verification of a timestamp-based checkpointing protocol. Furthermore, during the process of verification, insights gained in such a stack of protocols have assisted in validating some additional properties those dealing with failure recovery.     

Specification and analysis of parallel/distributed software andsystems by Petri nets with transition enabling functions

An approach for visually specifying parallel/distributed software using Petri nets (PNs) extend with transition enabling functions (TEFs) is investigated. The approach is demonstrated to be useful in the specification of decision-making activities that control distributed computing systems. PNs are employed because of their highly visual nature that can give insight into the nature of the controller of such a system and because of their analytical properties. In order to increase the expressive power of PNs, the extension of TEFs is used. The main focus is the specification and analysis of parallel/distributed software and systems. A key element of this approach is a set of rules derived to automatically transform such an extended net into a basic PN. Once the rules have been applied to transform the specification, analytical methods can be used to investigate characteristic properties of the system and validate correct operation     

Architecting Fault Tolerance with Exception Handling: Verification and Validation

When building dependable systems by integrating untrusted software components that were not originally designed to interact with each other, it is likely the occurrence of architectural mismatches related to assumptions in their failure behaviour. These mismatches, if not prevented during system design, have to be tolerated during runtime. This paper presents an architectural abstraction based on exception handling for structuring fault-tolerant software systems. This abstraction comprises several components and connectors that promote an existing untrusted software element into an idealised fault-tolerant architectural element. Moreover, it is considered in the context of a rigorous software development approach based on formal methods for representing the structure and behaviour of the software architecture. The proposed approach relies on a formal specification and verification for analysing exception propagation, and verifying important dependability properties, such as deadlock freedom, and scenarios of architectural reconfiguration. The formal models are automatically generated using model transformation from UML diagrams: component diagram representing the system structure, and sequence diagrams representing the system behaviour. Finally, the formal models are also used for generating unit and integration test cases that are used for assessing the correctness of the source code. The feasibility of the proposed architectural approach was evaluated on an embedded critical case study. Patrick Brito is supported by Fapesp/Brazil under Grant No. 06/02116–2 and CAPES/Brazil under Grant No. 0722–07–3. Cecília Rubira is partially supported by CNPq/Brazil under Grant Nos. 301446/2006–7 and 484138/2006–5.     

A toolset in Java2 for modelling, prototyping and implementing communicating real-time state machines

This paper proposes an approach to the development of real-time systems which depends on Communicating Real-Time State Machines (CRSMs) as the specification language, and on a customisable actor kernel for prototyping, analysis and implementation of a modelled system. CRSMs offer an intuitive and distributed specification of a system in terms of a collection of co-operating state machines interacting with one another through timed CSP-like I/O commands. On the other hand, the underlying actor framework provides a time-sensitive scheduling structure which can be tuned to CSRMs in order to support temporal validation through assertions on the recorded time-stamped event histories. The approach can be practically used through a graphical environment (jCRSM) which has been realised using Java2. The toolset facilitates editing, testing and implementation in Java of CRSM systems. The proposed methodology is novel in that it provides a seamless system development life cycle where the specification, analysis, design and implementation phases are unified by a common representation of machines in terms of actors. The paper demonstrates the use of CRSM based software components by means of examples.     

Realizability of concurrent recursive programs

We study the realizability problem for concurrent recursive programs: given a distributed system architecture and a sequential specification over words, find a distributed automata implementation that is equivalent to the specification. This problem is well-studied as far as finite-state processes are concerned, and it has a solution in terms of Zielonka’s Theorem. We lift Zielonka’s Theorem to the case where processes are recursive and modeled as visibly pushdown (or, equivalently, nested-word) automata. However, contrarily to the finite-state case, it is undecidable whether a specification is realizable or not. Therefore, we also consider suitable underapproximation techniques from the literature developed for multi-pushdown systems, and we show that they lead to a realizability framework with effective algorithms.     

Applying techniques and tools for the performance engineering of SDL systems

The integration of performance evaluation techniques into the SDL method is an important task. In particular in the area of telecommunications and distributed systems where product families have to be maintained for many years, performance should be considered from the very beginning of system design. This paper demonstrates how performance engineering can be successfully applied. Firstly, an SDL specification of TCP/IP is used to derive a performance model that includes the original SDL system as well as additional constructs describing the consumption of time and resources. Different implementation variants have been evaluated in experimental scenarios. Secondly, the application of a specification-driven monitoring technique to the same SDL specification of TCP/IP is described. The case study shows how the functional and temporal behaviour of an implementation derived from an SDL specification can be analysed and improved by monitoring the running system. The two approaches, modelling and monitoring, are supplementary to each other. This paper provides arguments that the systematic application of specification-driven performance engineering will result in major savings of time and money in later development phases and for later system releases.     

The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems

Modern software systems must support a high degree of variability to accommodate a wide range of requirements and operating conditions. This paper introduces the Abstract Behavioural Specification (ABS) language and tool suite, a comprehensive platform for developing and analysing highly adaptable distributed concurrent software systems. The ABS language has a hybrid functional and object- oriented core, and comes with extensions that support the development of systems that are adaptable to diversified requirements, yet capable to maintain a high level of trustworthiness. Using ABS, system variability is consistently traceable from the level of requirements engineering down to object behaviour. This facilitates temporal evolution, as changes to the required set of features of a system are automatically reflected by functional adaptation of the system’s behaviour. The analysis capabilities of ABS stretch from debugging, observing and simulating to resource analysis of ABS models and help ensure that a system will remain dependable throughout its evolutionary lifetime. We report on the experience of using the ABS language and the ABS tool suite in an industrial case study.     

A classification of total order specifications and its application to fixed sequencer-based implementations

During the last two decades the design and development of total order (TO) communications has been one of the main research topics in dependable distributed computing. The huge amount of research work has produced several TO specifications and a wide variety of TO implementations with different guarantees whose differences are often left hidden or unclear. This paper presents a systematic classification of six distinct TO specifications based on a well-defined formal framework. The classification allows us (i) to define in a formal way the differences among the behaviors of faulty and correct processes admitted by each specification, and (ii) to easily match TO implementations with respect to their enforced specification. The classification is applied to study the properties of eight variations of TO implementations based on a fixed sequencer given in a well-known context, namely primary component group communication systems.     

Specification and analysis of real-time systems with PARAGON

This paper describes a methodology for the specification and analysis of distributed real-time systems using the toolset called PARAGON. PARAGON is based on the Communicating Shared Resources paradigm, which allows a real-time system to be modeled as a set of communicating processes that compete for shared resources. PARAGON supports both visual and textual languages for describing real-time systems. It offers automatic analysis based on state space exploration as well as user-directed simulation. Our experience with using PARAGON in several case studies resulted in a methodology that includes design patterns and abstraction heuristics, as well as an overall process. This paper briefly overviews the communicating shared resource paradigm and its toolset PARAGON, including the textual and visual specification languages. The paper then describes our methodology with special emphasis on heuristics that can be used in PARAGON to reduce the state space. To illustrate the methodology, we use examples from a real-life system case study. This revised version was published online in June 2006 with corrections to the Cover Date.     

基于工作流管理技术的网上购物仿真系统

介绍了工作流管理系统的基本概念和建模方法,引入工作流组织模型和过程模型的语言,并将它们运用于网上购物仿真系统的设计和实现,为分布式系统集成提出了一种新的方法。     

A framework for determining design correctness

Quality is one of the main concerns in today's systems and software development and use. One important instrument in verification is the use of formal methods, which means that requirements and designs are analyzed formally to determine their relationships. Furthermore, since professional software design is to an increasing extent a distributed process, the issue of integrating different systems to an entity is of great importance in modern system development and design. Various candidates for formalizing system development and integration have prevailed, but very often, particularly for dynamic conflict detection, these introduce non-standard objects and formalisms, leading to severe confusion, both regarding the semantics and the computability. In contrast to such, we introduce a framework for defining requirement fulfillment by designs, detecting conflicts of various kinds as well as integration of heterogeneous schemata. The framework introduced transcends ordinary logical consequence, as it takes into account static and dynamic aspects of design consistency and, in particular, the specific features of the state space of a specification. Another feature of the approach is that it provides a unifying framework for design conflict analysis and schema integration.     

Graph-based reasoning in collaborative knowledge management for industrial maintenance

Capitalization and sharing of lessons learned play an essential role in managing the activities of industrial systems. This is particularly the case for the maintenance management, especially for distributed systems often associated with collaborative decision-making systems. Our contribution focuses on the formalization of the expert knowledge required for maintenance actors that will easily engage support tools to accomplish their missions in collaborative frameworks. To do this, we use the conceptual graphs formalism with their reasoning operations for the comparison and integration of several conceptual graph rules corresponding to different viewpoint of experts. The proposed approach is applied to a case study focusing on the maintenance management of a rotary machinery system.     

Ready for testing: ensuring conformance to industrial standards through formal verification

The design of distributed, safety-critical real-time systems is challenging due to their high complexity, the potentially large number of components, and complicated requirements and environment assumptions that stem from international standards. We present a case study that shows that despite those challenges, the automated formal verification of such systems is not only possible, but practicable even in the context of small to medium-sized enterprises. We considered a wireless fire alarm system, regulated by the EN 54 standard. We performed formal requirements engineering, modeling and verification and uncovered severe design flaws that would have prevented its certification. For an improved design, we provided dependable verification results which in particular ensure that certification tests for a relevant regulation standard will be passed. In general we observe that if system tests are specified by generalized test procedures, then verifying that a system will pass any test following those test procedures is a cost-efficient approach to improve the product quality based on formal methods. Based on our experience, we propose an approach useful to integrate the application of formal methods to product development in SME.     

Integrating methods of human-computer interface design with structured systems development

Various methods for specification and design of the human-computer interface have been proposed but practice of such methods is not widespread. Possible reasons for this may be the lack of integration of human-computer interface design with software engineering and the specialized nature of HCI methods. A method of interface design is proposed which integrates the development of the human-computer interface with structured systems analysis and design. The method covers task and user analysis, interface specification and dialogue design. A case study of a library system is used to illustrate the method which is discussed in relation to different approaches that have been adopted for interface specification and design. It is argued that software design methods should cover all aspects of process design and the human-computer interface.     

On the use of a formal requirements engineering language: The Generalized Railroad Crossing Problem

In this paper, we report on the use of theAlbert II requirements specification language through the handling of the Generalized Railroad Crossing case study. This formal language is based on an ontology of concepts used for capturing requirements inherent in real-time, distributed systems. Because of itsnaturalness, the language supports a direct mapping of customers’ informal needs onto formal statements, without having to introduce artificial elements. The language is founded on a formal framework (real-time temporal logic) which supports the reasoning process of the analyst during the elaboration of the specification. Such support for the reasoning is illustrated in the context of a goal-oriented approach adopted for the elaboration of the case study.     

Specifying distributed multi-agent systems in chemical reaction metaphor

This paper presents an application of Chemical Reaction Metaphor (CRM) in distributed multi-agent systems (MAS). The suitability of using CRM to model multi-agent systems is justified by CRM's capacity in specifying dynamic features of multi-agent systems. A case study in an agent-based e-learning system (course material updating) demonstrates how the CRM based language, Gamma, can be used to specify the architectures of multi-agent systems. The effectiveness of specifying multi-agent systems in CRM from the view point of software engineering is further justified by introducing a transformational method for implementing the specified multi-agent systems. A computation model with a tree-structured architecture is proposed to base the design of the specified multi-agent system during the implementation phase. A module language based on the computation model is introduced as an intermediate language to facilitate the translation of the specification of multi-agent systems. The multicast networking technology pragmatizes the implementation of communications and synchronization among distributed agents. The paper also discusses the feasibility of implementing an automatic translation from the Gamma specification to a program in the module language. This work is supported by University of Houston-Downtown Organized Research Committee.