Java-MaC: A Run-time Assurance Tool for Java Programs

We describe Java-MaC, a prototype implementation of the Monitoring and Checking (MaC) architecture for Java programs. The MaC architecture provides assurance about the correct execution of target programs at run-time. Monitoring and checking is performed based on a formal specification of system requirements. MaC bridges the gap between formal verification, which ensures the correctness of a design rather than an implementation, and testing, which only partially validates an implementation. Java-MaC provides a lightweight formal method solution as a viable complement to the current heavyweight formal methods. An important aspect of the architecture is the clear separation between monitoring implementation-dependent low-level behaviors and checking high-level behaviors against a formal requirements specification. Another salient feature is automatic instrumentation of executable codes. The paper presents an overview of the MaC architecture and a prototype implementation Java-MaC.     

Error Detection in Concurrent Java Programs

Concurrency in multithreaded programs introduces additional complexity in software verification and testing, and thereby significantly increases the cost of Quality Assurance (QA). We present a case study in which a specialized model checker was used to discover concurrency errors in a large preexisting code base. The results revealed race conditions that lead to data corruption errors whose detection would have been prohibitively expensive with conventional testing and QA methods. We describe our methodology and highlight parts of the methodology that could be automated.     

A Platform-Independent Distributed Runtime for Standard Multithreaded Java

JavaSplit is a portable runtime environment for distributed execution of standard multithreaded Java programs. It gains augmented computational power and increased memory capacity by distributing the threads and objects of an application among the available machines. Unlike previous works, which either forfeit Java portability by using a nonstandard Java Virtual Machine (JVM) or compromise transparency by requiring user intervention in making the application suitable for distributed execution, JavaSplit automatically executes standard multithreaded Java on any heterogenous collection of Java-enabled machines. Each machine carries out its part of the computation using nothing but its local standard (unmodified) JVM. Neither the programmer nor the person submitting the program for execution needs to be aware of JavaSplit or its distributed nature. We evaluate the efficiency of JavaSplit on several combinations of operating systems, JVM implementations, and communication hardware.     

A Systematic Approach to the Petri Net Based Specification of Concurrent Systems

We describe an approach to the specification of concurrent systems which enables a Petri net model of a system to be built up in a systematic way starting from a trace-based CSP specification. This method enables the separate specification of the behavior of each component (process) and their interactions in terms of the feasible sequences of events in which they can be involved. A set of rules is then applied to transform the trace-based specifications into a complete Petri net that is analyzed and/or executed to validate system behavior. The domain transformation procedure is fully automatable. The specification of a safety-critical railway control system is used as a case study.     

A Model for Slicing JAVA Programs Hierarchically

Program slicing can be effectively used to debug, test, analyze, understand and maintain objectoriented software. In this paper, a new slicing model is proposed to slice Java programs based on their inherent hierarchical feature. The main idea of hierarchical slicing is to slice programs in a stepwise way, from package level, to class level, method level, and finally up to statement level. The stepwise slicing algorithm and the related graph reachability algorithms are presented, the architecture of the Java program Analyzing TOol (JATO) based on hierarchical slicing model is provided, the applications and a small case study are also discussed.     

Prospec: Support for Elicitation and Formal Specification of Software Properties

Although formal verification techniques have been demonstrated to improve program dependability, software practitioners have not widely adopted them. One reason often cited is the difficulty in writing formal specifications. This paper introduces Prospec, a tool to assist practitioners in formally specifying software properties. Prospec uses property patterns and scopes. Previous efforts at providing tool support for property specification have not provided convenient abstractions for specifying properties that include multiple events or conditions. A taxonomy of composite propositions is introduced to address this issue by defining relations among propositions and providing graphical abstractions that can assist in specification and validation of properties. This paper shows how composite propositions can enhance the specification pattern system by helping practitioners consider subtleties of behavior in sequences and concurrency through directed questions and visual abstractions. The paper introduces an elicitation and specification process to define patterns, scopes, and composite propositions.     

Ann: A domain-specific language for the effective design and validation of Java annotations

This paper describes a new modelling language for the effective design and validation of Java annotations. Since their inclusion in the 5th edition of Java, annotations have grown from a useful tool for the addition of meta-data to play a central role in many popular software projects. Usually they are not conceived in isolation, but in groups, with dependency and integrity constraints between them. However, the native support provided by Java for expressing this design is very limited.To overcome its deficiencies and make explicit the rich conceptual model which lies behind a set of annotations, we propose a domain-specific modelling language. The proposal has been implemented as an Eclipse plug-in, including an editor and an integrated code generator that synthesises annotation processors. The environment also integrates a model finder, able to detect unsatisfiable constraints between different annotations, and to provide examples of correct annotation usages for validation. The language has been tested using a real set of annotations from the Java Persistence API (JPA). Within this subset we have found enough rich semantics expressible with Ann and omitted nowadays by the Java language, which shows the benefits of Ann in a relevant field of application.     

A unified formal basis for the CASE tools system

XYZ system is a CASE tools system based on a temporal logic language XYZ/E which can represent every essential feature of conventional HLL's (sequential or concurrent), specifications of different levels, production rules, operational semantics of graphic languages in a uniform framework. With this formal language as the common basis, all the CASE tools including various kinds of graphic tools for distributed process, concurrent programs with phased memory and sequential programs, tools for verification, rapid-prototyping, language transformation, and module management can be connected freely to form more sophisticated and integrated systems.     

Mobile Java RMI support over heterogeneous wireless networks: A case study

Distributed object-oriented platforms are increasingly important in wireless environments to provide frameworks for collaborative computation and for managing a large pool of distributed resources. One of the important layers for implementing distributed computing in such environments is via remoting mechanisms. For example, Java uses Remote Method Invocation (RMI) for handling distributed controls. In this paper, we investigate the support for this important layer on wireless environments and address the issues to support Java RMI over heterogeneous wireless environments. We present a case study for supporting Java RMI in Bluetooth, GPRS, and WLAN environments, which represents an important middleware for component communications. The Bluetooth layer is supported by incorporating a set of protocol stack layers for Bluetooth, known as JavaBT that has been developed by us, and by supporting an L2CAP layer with sockets to support Java RMI sockets. RMI over GPRS/WLAN is achieved by RMI implementation over IP layer. Our support for the roaming of Java RMI over heterogeneous wireless networks is based on the concept of direct connection, which avoids the problems caused by forwarding. The difficulty of this strategy is how to handle the existing connection when the mobile node moves to another location so as to avoid interruption of the high-level applications. We solve this problem in Java RMI by the support of dynamic addresses and dynamic sockets. We also propose algorithms to handle the handoff process. In addition, methods for connect-loss detection and data-integrity maintenance in dealing with roaming scenarios are also presented. Java Grande benchmarks are used to demonstrate that our RMI implementations over GPRS, WLAN, and Bluetooth networks are effective in supporting parallel and distributed control of Java layers in heterogeneous wireless environments.     

A Method for Developing Component-Oriented Applications: A Use-Context Driven Approach Toward Component Coordination

In this paper, we propose a methodology for the development of component-oriented applications based on the Component Coordination Model (CCM) that is embedded into applications during software architecture design. The method is general enough to support the conceptual level of component-based software development. It provides a set of guidelines that ease developers during analysis and design phases. These guidelines are defined as processes for developing increasingly detailed models of constructing software systems. The CCM is driven by the use-context model, which directly reflects the role model that abstracts system behaviors as a computational organization comprising various role relationships. It then focuses on exposing the design of software components to be separated from their execution contexts. These separate concerns, including computation, coordination, and policies imposed on a given use-context, form the principal concept of our approach. A case study using the proposed method has been demonstrated in order to provide the feasibility of the introduced approach.     

MOBMAS: A methodology for ontology-based multi-agent systems development

Ontologies offer significant benefits to multi-agent systems: interoperability, reusability, support for multi-agent system (MAS) development activities (such as system analysis and agent knowledge modeling) and support for MAS operation (such as agent communication and reasoning). This paper presents an ontology-based methodology, MOBMAS, for the analysis and design of multi-agent systems. MOBMAS is the first methodology that explicitly identifies and implements the various ways in which ontologies can be used in the MAS development process and integrated into the MAS model definitions. In this paper, we present comprehensive documentation and validation of MOBMAS.     

The software information base: A server for reuse

We present an experimental software repository system that provides organization, storage, management, and access facilities for reusable software components. The system, intended as part of an applications development environment, supports the representation of information about requirements, designs and implementations of software, and offers facilities for visual presentation of the soft-ware objects. This article details the features and architecture of the repository system, the technical challenges and the choices made for the system development along with a usage scenario that illustrates its functionality. The system has been developed and evaluated within the context of the ITHACA project, a technology integration/software engineering project sponsored by the European Communities through the ESPRIT program, aimed at developing an integrated reuse-centered application development and support environment based on object-oriented techniques.     

Interweaving knowledge extracting,organizing and evaluating: A concrete design for preventing logic and structure bugs while interviewing experts

The process of constructing expert systems (ESs), programs that approximate how domain experts solve problems in their specialized fields, is not at all as systematic, efficient, and verifiable as it should be. A reason is that no rigorous error-prevention interviewing method exists for structuring and testing ESs while building them. Often domain experts do implicitly ask of themselves analytical questions such as ‘Is that claim of mine always true?’ Another kind of expert — one specializing in logic analysis — explicitates, collects, and systematizes the fund of generic questions, such as ‘Are these sub-goals sufficient steps to the pre-established goal-category?’ There is a great need to make a method of interviewing, interlaced with testing and organizing, available to all domain experts and ES programmers via an interactive program. This program, which can generically be called a LAP (Logic Aids Program), plays the role of a domain-independent logic-assistant.     

A survey of tools for the validation and verification of knowledge-based systems: 1985-1995

This paper presents the findings of a survey of software tools built to assist in the verification and validation of knowledge-based systems. The tools were identified from literature sources from the period 1985-1995. The tool builders were contacted and asked to complete and return a survey that identified which testing and analysis techniques were utilised and covered by their tool. From these survey results it is possible to identify trends in tool development, technique coverage and areas for future research.     

Requirements Reuse for Improving Information Systems Security: A Practitioner’s Approach

Information systems security issues have usually been considered only after the system has been developed completely, and rarely during its design, coding, testing or deployment. However, the advisability of considering security from the very beginning of the system development has recently begun to be appreciated, and in particular in the system requirements specification phase. We present a practical method to elicit and specify the system and software requirements, including a repository containing reusable requirements, a spiral process model, and a set of requirements documents templates. In this paper, this method is focused on the security of information systems and, thus, the reusable requirements repository contains all the requirements taken from MAGERIT, the Spanish public administration risk analysis and management method, which conforms to ISO 15408, Common Criteria Framework. Any information system including these security requirements must therefore pass a risk analysis and management study performed with MAGERIT. The requirements specification templates are hierarchically structured and are based on IEEE standards. Finally, we show a case study in a system of our regional administration aimed at managing state subsidies.