18649413
Capturing periodic concurrent interactions of mission computer tasks
Safety critical systems, such as aviation systems controlled by software, often have hard real-time requirements. Producing the correct result at the right time is the fundamental goal of such systems. Formally specifying the system functions and the timing requirements is the crucial step towards achieving such a goal. Aviation systems often need to be modified or upgraded on a regular basis, i.e. functionality and timing constraints may be altered. Therefore, the formal specification of such systems needs to be easily reused, maintained and modified. This paper demonstrates how the task scheduling aspects of an aircraft mission computer can be formalised in TCOZ.
18404140
Deep Semantic Links of TCSP and Object-Z: TCOZ Approach
Abstract. Formal methods can be used in effective combination only if the semantic links between individual methods are clearly established. This paper discusses the semantic design of TCOZ, a language blended from Object-Z and TCSP. The semantic model adopted is the infinite timed failures model of TCSP, extended to include initial state and update events for modelling operations on internal state. An infinite trace model has been used so as to ensure proper account is taken of the potentially unbounded non-determinism allowed by Z schemas.
15362726
State, event, time and diagram in system modeling
The design of complex systems requires powerful mechanisms for modeling state, concurrent events, and real-time behavior; as well as for visualising and structuring systems in order to control complexity. Methods integration has become a recent research trend in software specification and design. In the graphical area, many object-oriented methods have merged into one, the Unified Modeling Language (UML) which combines various diagrammatic modeling techniques to model static and dynamic aspects of software systems. Although traditional formal methods have not scale-up well, new integrated formal methods show great promise. This tutorial will present the state of the art in formal modeling techniques (state-based Object-Z and event-based Timed CSP), their integration (TCOZ), and transformation techniques from the integrated formalism to UML diagrams. An XML web environment for projecting integrated formal models to UML diagrams will also be demonstrated.
5239234
The role of secondary attributes in formal object modelling
When modelling a large and complex system, clarity of the specification becomes an important factor. In object-oriented specification, the states of individual objects are captured by the values of their attributes. Frequently however, there are dependencies between the attributes of an object. An appropriate indication of which attributes are primary (independent) and which are secondary (dependent) can add significantly to clarity. This paper details the notion of secondary attributes, their roles and implications in formal object-oriented specification.
13839820
Relating /spl pi/-calculus to Object-Z
Software systems have become increasingly distributed, dynamic and mobile. The complex state and dynamic interfaces of software components and their concurrent interactions provide challenging research issues in system specification and design. An effective combination of structured state-based formalism and dynamic action-based calculus may be a good solution for modeling complex distributed mobile systems. In this paper, we investigate the semantic links between Object-Z and /spl pi/ calculus and consequently introduce a powerful specification technique PiOZ that brings the strengths of the two together. The operational semantics of PiOZ integrates state transition semantics of Object-Z and /spl pi/-calculus reduction rules. The typing rules of PiOZ are developed and reasoning of a system property is presented.
10062286
Integrating Object-Z with timed automata
When designing a complex system, Object-Z is a powerful logic-based language for modeling the system state aspects, and timed automata is an excellent graph-based notation for capturing timed control behaviour of the system. This paper presents an effective combination of the two techniques with novel composition and communication mechanisms. The combined notation enhances Object-Z with realtime modeling capability and also extends timed automata with enhanced structure and state modeling features.
16840990
Automating the analysis of design component contracts
Software patterns are a new design paradigm used to solve problems that arise when developing software within a particular context. Patterns capture the static and dynamic structure and collaboration among the components in a software design. A key promise of the pattern-based approach is that it may greatly simplify the construction of software systems out of building blocks and thus reuse experience and reduce cost. However, it also introduces significant problems in ensuring the integrity and reliability of these composed systems because of their complex software topologies, interactions and transactions. There is a need to capture these features as a contract through a formal model that allows us to analyze pattern-based designs. In this paper, we provide an overview of a formal framework for ensuring the integrity of the compositions in object-oriented designs by providing mathematically rigorous modeling and analysis techniques for object-oriented systems comprising pattern-based designs as the basic building blocks or design components. A case study related to a hypermedia Web-based application has been presented to illustrate our approach in distributed systems. Copyright © 2005 John Wiley & Sons, Ltd.
12466739
UML Extensions for Design Pattern Compositions
Design patterns document good solutions to recurring problems in a particular context. Composing design patterns may achieve higher level of reuse by solving a set of problems. Design patterns and their compositions are usually modeled by UML diagrams. When a design pattern is applied or composed with other patterns, the pattern-related information may be lost because traditional UML diagrams do not track this information. Thus, it is hard for a designer to identify a design pattern when it is applied or composed. In this paper, we present notations to explicitly represent each pattern in the applications and compositions of design patterns. The notations allow us to maintain pattern-related information. Thus, a design pattern is identifiable and traceable from its application and composition with others.
6426341
Event-based blackboard architecture for multi-agent systems
Developing large multi-agent systems is a complex task involving the processes of the requirement, architecture, design and implementation of these systems. In particular, the architectural design is critical to cope with the increasing size and complexity of these systems. The multi-agent system that accesses a central repository is typically based on the blackboard architectural pattern. However, the control strategies of the agents are inherently complex. In this paper, we present an event-based control strategy to manage the access of central repository by multi-agents. In this approach, the blackboard pattern is composed with the implicit invocation pattern to separate the control policies from the control component so that the architecture is ease of evolution, reuses and changes.
26263616
Developing a Formal Design Analysis Framework
9559762
A logical framework for design composition
The design of a large component based software system typically involves the composition of different components. The lack of rigorous reasoning about the correctness of composition is an important barrier towards the promise of "plug and play". The author describes a rigorous logic framework to reason about component compositions. We focus our analysis on design components such as design patterns, which have been used by a large number of applications. We also propose methods to verify structural and behavioral composition correctness.