12666680
Semantic Web Languages - Towards an Institutional Perspective
The Semantic Web (SW) is viewed as the next generation of the Web that enables intelligent software agents to process and aggregate data autonomously. Ontology languages provide basic vocabularies to semantically markup data on the SW. We have witnessed an increase of numbers of SW languages in the last years. These languages, such as RDF, RDF Schema (RDFS), the OWL suite of languages, the OWL− − suite, SWRL, are based on different semantics, such as the RDFS-based, description logic-based, Datalog-based semantics. The relationship among the various semantics poses a challenge for the SW community for making the languages interoperable. Institutions provide a means of reasoning about software specifications regardless of the logical system. This makes it an ideal candidate to represent and reason about the various languages in the Semantic Web. In this paper, we construct institutions for the SW languages and use institution morphisms to relate them. We show that RDF framework together with the RDF serializations of SW languages form an indexed institution. This allows the use of Grothendieck institutions to combine Web ontologies described in various languages.
207130315
Formal Designs for Embedded and Hybrid Systems
The design of embedded and hybrid systems requires powerful mechanisms for modeling data, state, concurrency and real-time behaviour. The {first} part of this paper illustrates a powerful design notation Timed Communicating Object Z (TCOZ) that has both channel based and sensor/actuator based interfaces. We believe that TCOZ is well suited for presenting more complete and coherent design models for complex embedded and hybrid systems. However, the challenge is how to analyze and check these models with tools support. One effective approach is to project (transform) the design models into multiple domains, then to use existing specialized tools in those domains to perform the checking and analyzing tasks. The second part of this paper demonstrates one particular projection from TCOZ designs to Timed Automata (TA) models so that TA model checkers can be used to check time related properties.
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.
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.
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.
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.
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.
14676361
Service Oriented Evolutions and Analyses of Design Patterns
The globalization of software development helps to reduce business cost by outsourcing software design and development tasks. However, it also poses new challenges on the collaboration and management of the development teams at multiple remote sites. Service-oriented approaches facilitate Web-based collaborations and reuses. In this paper, we propose a service-oriented architecture for the collaboration of software design teams in distributed locations. In particular, our approach allows different design teams from multiple remote sites to design software systems with design patterns, to evolve the designs, and to check the consistencies of the design evolutions. We provide service-oriented prototype tools for the design teams from different physical locations to model the software system designs in UML, to evolve the designs based on XSLT transformations, and to check the consistencies based on the Java theorem prover. A case study is presented to illustrate our approach
10543361
Commutability of Design Pattern Instantiation and Integration
Design patterns capture expert design experience in generic design structure and behavior. A design pattern needs to be instantiated before using. It can be integrated with other patterns as well. The instantiation and integration operations are two important operations when a designer uses a design pattern in a particular application. In this paper, we investigate the commutability of these two operations based on our formal specification framework. We provide rigorous proofs on the conditions when the order of these two operations does not matter. Our results enable the software designers to choose their design processes with assurance of their equivalence.
44442404
Integrated 3-D Animation System for Decentralized Controlled Space Telescope Test-bed
5225607
Correct Composition of Design Components
In this paper, we describe a method for the composition of components that are relatively correct under a particular criterion. The notion of composition pattern is also introduced to reuse composition solutions to routine component composition problems. Once a composition pattern is proven correct, its instances can be reused many times. Thus, we propose reusing compositions as well as reusing components. The main points are illustrated by an example of the composition of two design patterns as design components. A proof of the correctness of two design patterns is provided.