Automatically Detecting and Visualising Errors in UML Diagrams

UML has become the de facto standard for object-oriented modelling. Currently, UML comprises several different notations with no formal semantics attached to the individual diagrams or their integration, thus preventing rigorous analysis of the diagrams. Previously, we developed a formalisation framework that attaches formal semantics to a subset of UML diagrams used to model embedded systems. This paper describes automated structural and behavioural analyses applicable to UML diagrams using our formalisation framework. In addition to intra- and inter-diagram consistency checks, we discuss how simulation and model checking can be used in tandem for behavioural analysis of the UML diagrams. Our tools also visually interpret the analysis results in terms of the original UML diagrams, thereby facilitating their correction and refinement. We illustrate these capabilities through the modelling and analysis of UML diagrams for an automotive industrial case study. Correspondence and offprint requests to: Dr B. Cheng, Software Engineering and Network Systems Laboratory, Department of Computer Science and Engineering, Michigan State University, 3115 Engineering Building, East Lansing, MI 48824, USA. Tel.: +1 517 355 8344; Fax: +1 517 432 1061; Email: chengb@cse.msu.edu     

Expressing checkable properties of dynamic systems: the Bandera Specification Language

Research on how to reason about correctness properties of software systems using model checking is advancing rapidly. Work on extracting finite-state models from program source code and on abstracting those models is focused on enabling the tractable checking of program properties such as freedom from deadlock and assertion violations. For the most part, the problem of specifying more general program properties has not been considered. In this paper, we report on the support for specifying properties of dynamic multi-threaded Java programs that we have built into the Bandera system. Bandera extracts finite-state models, in the input format of several existing model checkers, from Java code based on the property to be checked. The Bandera Specification Language (BSL) provides a language for defining general assertions and pre/post conditions on methods. It also supports the definition of observations that can be made of the state of program objects and the incorporation of those observations as predicates that can be instantiated in the scope of object quantifiers and used in describing common forms of state/event sequencing properties. We illustrate how BSL can be used to formulate a variety of system correctness properties for several multi-threaded Java applications. Published online: 2 October 2002     

The impact of object technology on commercial transaction processing

Businesses today are searching for information solutions that enable them to compete in the global marketplace. To minimize risk, these solutions must build on existing investments, permit the best technology to be applied to the problem, and be manageable. Object technology, with its promise of improved productivity and quality in application development, delivers these characteristics but, to date, its deployment in commercial business applications has been limited. One possible reason is the absence of the transaction paradigm, widely used in commercial environments and essential for reliable business applications. For object technology to be a serious contender in the construction of these solutions requires: – technology for transactional objects. In December 1994, the Object Management Group adopted a specification for an object transaction service (OTS). The OTS specifies mechanisms for defining and manipulating transactions. Though derived from the X/Open distributed transaction processing model, OTS contains additional enhancements specifically designed for the object environment. Similar technology from Microsoft appeared at the end of 1995. – methodologies for building new business systems from existing parts. Business process re-engineering is forcing businesses to improve their operations which bring products to market. Workflow computing, when used in conjunction with “object wrappers” provides tools to both define and track execution of business processes which leverage existing applications and infrastructure. – an execution environment which satisfies the requirements of the operational needs of the business. Transaction processing (TP) monitor technology, though widely accepted for mainframe transaction processing, has yet to enjoy similar success in the client/server marketplace. Instead the database vendors, with their extensive tool suites, dominate. As object brokers mature they will require many of the functions of today's TP monitors. Marrying these two technologies can produce a robust execution environment which offers a superior alternative for building and deploying client/server applications. Edited by Andreas Reuter, Received February 1995 / Revised August 1995 / Accepted May 1996     

Managing the verification trajectory

In this paper we take a closer look at the automated analysis of designs, in particular of verification by model checking. Model checking tools are increasingly being used for the verification of real-life systems in an industrial context. In addition to ongoing research aimed at curbing the complexity of dealing with the inherent state space explosion problem – which allows us to apply these techniques to ever larger systems – attention must now also be paid to the methodology of model checking, to decide how to use these techniques to their best advantage. Model checking “in the large” causes a substantial proliferation of interrelated models and model checking sessions that must be carefully managed in order to control the overall verification process. We show that in order to do this well both notational and tool support are required. We discuss the use of software configuration management techniques and tools to manage and control the verification trajectory. We present Xspin/Project, an extension to Xspin, which automatically controls and manages the validation trajectory when using the model checker Spin. Published online: 18 June 2002     

Translating Java for Multiple Model Checkers: The Bandera Back-End

One approach to model checking program source code is to view a model checker as a target machine. In this setting, program source code is translated to a model checker’s input language using a process that shares much in common with program compilation. For example, well-defined intermediate program representations are used to stage the translation through a series of analyses and optimizing transformations and target-specific details are isolated in code generation modules.In this paper, we present the Bandera Intermediate Representation (BIR)—a guarded-assignment transformation system language that has been designed to support the translation of Java programs to a variety of model checkers. BIR includes constructs, such as inheritance, dynamic creation of data, and locking primitives, that are designed to model the semantics of Java primitives. BIR also includes several non-deterministic choice constructs that support abstraction in modeling and specification of properties of dynamic heap structures.We have developed a BIR-based tool infrastructure that has been applied to develop customized analysis frameworks for several different input languages using different model checking tools. We present BIR’s type system and operational semantics in sufficient detail to support similar applications by other researchers. This semantics details several state space reductions and state space search variations. We describe the translation of Java to BIR and how BIR is translated to the input languages of several model checkers.     

Verification and optimization of a PLC control schedule

We report on the use of model checking techniques for both the verification of a process control program and the derivation of optimal control schedules. Most of this work has been carried out as part of a case study for the EU VHS project (Verification of Hybrid Systems), in which the program for a Programmable Logic Controller (PLC) of an experimental chemical plant had to be designed and verified. The original intention of our approach was to see how much could be achieved here using the standard model checking environment of SPIN/Promela. As the symbolic calculations of real-time model checkers can be quite expensive it is interesting to try and exploit the efficiency of established non-real-time model checkers like SPIN in those cases where promising work-arounds seem to exist. In our case we handled the relevant real-time properties of the PLC controller using a time-abstraction technique; for the scheduling we implemented in Promela a so-called variable time advance procedure . To compare and interpret the results we carried out the same case study with the aid of the real-time model checker Uppaal, enhanced with facilities for cost-guided state space exploration. Both approaches proved sufficiently powerful to verify the design of the controller and/or derive (time-)optimal schedules within reasonable time and space requirements. Published online: 2 October 2002 The work reported here was carried out while the second and third authors were employed by the Computer Science Department of the University of Nijmegen, Netherlands. The second author was supported by an NWO postdoc grant, the third author by an NWO PhD grant, and both were supported by the EU LTR project VHS (Project No. 26270).     

Approximate query processing using wavelets

Approximate query processing has emerged as a cost-effective approach for dealing with the huge data volumes and stringent response-time requirements of today's decision support systems (DSS). Most work in this area, however, has so far been limited in its query processing scope, typically focusing on specific forms of aggregate queries. Furthermore, conventional approaches based on sampling or histograms appear to be inherently limited when it comes to approximating the results of complex queries over high-dimensional DSS data sets. In this paper, we propose the use of multi-dimensional wavelets as an effective tool for general-purpose approximate query processing in modern, high-dimensional applications. Our approach is based on building wavelet-coefficient synopses of the data and using these synopses to provide approximate answers to queries. We develop novel query processing algorithms that operate directly on the wavelet-coefficient synopses of relational tables, allowing us to process arbitrarily complex queries entirely in the wavelet-coefficient domain. This guarantees extremely fast response times since our approximate query execution engine can do the bulk of its processing over compact sets of wavelet coefficients, essentially postponing the expansion into relational tuples until the end-result of the query. We also propose a novel wavelet decomposition algorithm that can build these synopses in an I/O-efficient manner. Finally, we conduct an extensive experimental study with synthetic as well as real-life data sets to determine the effectiveness of our wavelet-based approach compared to sampling and histograms. Our results demonstrate that our techniques: (1) provide approximate answers of better quality than either sampling or histograms; (2) offer query execution-time speedups of more than two orders of magnitude; and (3) guarantee extremely fast synopsis construction times that scale linearly with the size of the data. Received: 7 August 2000 / Accepted: 1 April 2001 Published online: 7 June 2001     

Dealing with forward and backward jumps in workflow management systems

Workflow management systems (WfMS) offer a promising technology for the realization of process-centered application systems. A deficiency of existing WfMS is their inadequate support for dealing with exceptional deviations from the standard procedure. In the ADEPT project, therefore, we have developed advanced concepts for workflow modeling and execution, which aim at the increase of flexibility in WfMS. On the one hand we allow workflow designers to model exceptional execution paths already at buildtime provided that these deviations are known in advance. On the other hand authorized users may dynamically deviate from the pre-modeled workflow at runtime as well in order to deal with unforeseen events. In this paper, we focus on forward and backward jumps needed in this context. We describe sophisticated modeling concepts for capturing deviations in workflow models already at buildtime, and we show how forward and backward jumps (of different semantics) can be correctly applied in an ad-hoc manner during runtime as well. We work out basic requirements, facilities, and limitations arising in this context. Our experiences with applications from different domains have shown that the developed concepts will form a key part of process flexibility in process-centered information systems. Received: 6 October 2002 / Accepted: 8 January 2003 Published online: 27 February 2003 This paper is a revised and extended version of [40]. The described work was partially performed in the research project “Scalability in Adaptive Workflow Management Systems” funded by the Deutsche Forschungsgemeinschaft (DFG).     

Constraint-based deductive model checking

We show that constraint logic programming (CLP) can serve as a conceptual basis and as a practical implementation platform for the model checking of infinite-state systems. CLP programs are logical formulas (built up from constraints) that have both a logical interpretation and an operational semantics. Our contributions are: (1) a translation of concurrent systems (imperative programs) into CLP programs with the same operational semantics; and (2) a deductive method for verifying safety and liveness properties of the systems which is based on the logical interpretation of the CLP programs produced by the translation. We have implemented the method in a CLP system and verified well-known examples of infinite-state programs over integers, using linear constraints here as opposed to Presburger arithmetic as in previous solutions. Published online: 18 July 2001     

EXACT: an extensible approach to active object-oriented databases

Active database management systems (DBMSs) are a fast-growing area of research, mainly due to the large number of applications which can benefit from this active dimension. These applications are far from being homogeneous, requiring different kinds of functionalities. However, most of the active DBMSs described in the literature only provide a fixed, hard-wired execution model to support the active dimension. In object-oriented DBMSs, event-condition-action rules have been propo sed for providing active behaviour. This paper presents EXACT, a rule manager for object-oriented DBMSs which provides a variety of options from which the designer can choose the one that best fits the semantics of the concept to be supported by rules. Due to the difficulty of foreseeing future requirements, special attention has been paid to making rule management easily extensible, so that the user can tailor it to suit specific applications. This has been borne out by an implementation in ADAM, an object -oriented DBMS. An example is shown of how the default mechanism can be easily extended to support new requirements. Edited by Y. Vassiliou. Received May 26, 1994 / Revised January 26, 1995, June 22, 1996 / Accepted November 4, 1996     

Developer-friendly verification of process-based systems

System quality is a key issue in modern systems development. Tool support is essential for checking the system quality efficiently. This is particularly true with respect to the dynamic interactions of the processes within a system. A first generation of checkers – model checkers – provide a basic technology for the verification of process-based systems.Conventional model checkers bear two drawbacks concerning mainly their user-friendliness which impede their broad application. First, model checkers in general do not support the graphical representation of rules (specifications). Although a model may be described with a graphical notation, the specification which has to be checked against the model is generally still text-based. This makes the usage of the checker difficult for process modeling experts. Second, the expressiveness concerning the verification model semantics to be checked is limited to states which are connected by transitions. However, many system development models (e.g. the business process model we use as example) embrace more element types. These are unsupported by the conventional model checkers resulting in a loss of verification precision.The checking system we present in this paper integrates both novelties: the graphical notation for a user-friendly specification and an extended specification language together with a corresponding verifier which supports the checking of many different types of elements (although the paper presents the approach with only two types). The integration is realized by an XML-based transformation system which links the graphical editor to the checking tool.     

Local model checking and protocol analysis

This paper describes a local model-checking algorithm for the alternation-free fragment of the modal mu-calculus that has been implemented in the Concurrency Factory and discusses its application to the analysis of a real-time communications protocol. The protocol considered is RETHER, a software-based, real-time Ethernet protocol developed at SUNY at Stony Brook. Its purpose is to provide guaranteed bandwidth and deterministic, periodic network access to multimedia applications over commodity Ethernet hardware. Our model-checking results show that (for a particular network configuration) RETHER makes good on its bandwidth guarantees to real-time nodes without exposing non-real-time nodes to the possibility of starvation. Our data also indicate that, in many cases, the state-exploration overhead of the local model checker is significantly smaller than the total amount that would result from a global analysis of the protocol. In the course of specifying and verifying RETHER, we also identified an alternative design of the protocol that warranted further study due to its potentially smaller run-time overhead in servicing requests for data transmission. Again, using local model checking, we showed that this alternative design also possesses the properties of interest. This observation points out one of the often-overlooked benefits of formal verification: by forcing designers to understand their designs rigorously and abstractly, these techniques often enable the designers to uncover interesting design alternatives.     

Access path support for referential integrity in SQL2

The relational model of data incorporates fundamental assertions for entity integrity and referential integrity. Recently, these so-called relational invariants were more precisely specified by the new SQL2 standard. Accordingly, they have to be guaranteed by a relational DBMS to its users and, therefore, all issues of semantics and implementation became very important. The specification of referential integrity embodies quite a number of complications including the MATCH clause and a collection of referential actions. In particular, turns out to be hard to understand and, if applied, difficult and expensive to maintain. In this paper, we identify the functional requirements for preserving referential integrity. At a level free of implementational considerations, the number and kinds of searches necessary for referential integrity maintenance are derived. Based on these findings, our investigation is focused on the question of how the functional requirements can be supported by implementation concepts in an efficient way. We determine the search cost for referential integrity maintenance (in terms of page references) for various possible access path structures. Our main result is that a combined access path structure is the most appropriatefor checking the regular MATCH option, whereas requires very expensive and complicated check procedures. If it cannot be avoided at all, the best support is achieved by a combination of multiple -trees. Edited by Alain Pirotte. Received June 28, 1993 / Revised August 19, 1994 / Accepted April 26, 1995     

Using vanishing points for camera calibration and coarse 3D reconstruction from a single image

In this paper, we show how to calibrate a camera and to recover the geometry and the photometry (textures) of objects from a single image. The aim of this work is to make it possible walkthrough and augment reality in a 3D model reconstructed from a single image. The calibration step does not need any calibration target and makes only four assumptions: (1) the single image contains at least two vanishing points, (2) the length (in 3D space) of one line segment (for determining the translation vector) in the image is known, (3) the principle point is the center of the image, and (4) the aspect ratio is fixed by the user. Each vanishing point is determined from a set of parallel lines. These vanishing points help determine a 3D world coordinate system R _o. After having computed the focal length, the rotation matrix and the translation vector are evaluated in turn for describing the rigid motion between R _o and the camera coordinate system R _c. Next, the reconstruction step consists in placing, rotating, scaling, and translating a rectangular 3D box that must fit at best with the potential objects within the scene as seen through the single image. With each face of a rectangular box, a texture that may contain holes due to invisible parts of certain objects is assigned. We show how the textures are extracted and how these holes are located and filled. Our method has been applied to various real images (pictures scanned from books, photographs) and synthetic images.     

Efficient debugging in a formal verification environment

In this paper, we emphasize the importance of efficient debugging in formal verification and present capabilities that we have developed in order to aid debugging in Intel’s Formal Verification Environment. We have given the name “Counter-Example Wizard” to the bundle of capabilities that we have developed to address the needs of the verification engineer in the context of counter-example diagnosis and rectification. The novel features of the Counter-Example Wizard are the multi-value counter-example annotation, constraint-based debugging, and multiple counter-example generation mechanisms. Our experience with the verification of real-life Intel designs shows that these capabilities complement one another and can help the verification engineer diagnose and fix a reported failure. We use real-life verification cases to illustrate how our system solution can significantly reduce the time spent in the loop of model checking, specification, and design modification. Published online: 21 February 2003     

A case study in class library verification: Java’s vector class

This paper presents a verification of an invariant property for the Vector class from JAVA’s standard library (API). The property says (essentially) that the actual size of a vector is less than or equal to its capacity. It is shown that this “safety” or “data integrity” property is maintained by all methods of the Vector class, and that it holds for all objects created by the constructors of the Vector class. The verification of the Vector class invariant is done with the proof tool PVS. It is based on a semantics of JAVA in higher order logic. The latter is incorporated in a special purpose compiler, the LOOP tool, which translates JAVA classes into logical theories. It has been applied to the Vector class for this case study. The actual verification takes into account the object-oriented character of JAVA: (non-final) methods may always be overridden, so that one cannot rely on a particular implementation. Instead, one has to reason from method specifications in such cases. This project demonstrates the feasibility of tool-assisted verification of non-trivial properties for non-trivial JAVA classes. Published online: 10 May 2001     

Supporting efficient multimedia database exploration

Due to the fuzziness of query specification and media matching, multimedia retrieval is conducted by way of exploration. It is essential to provide feedback so that users can visualize query reformulation alternatives and database content distribution. Since media matching is an expensive task, another issue is how to efficiently support exploration so that the system is not overloaded by perpetual query reformulation. In this paper, we present a uniform framework to represent statistical information of both semantics and visual metadata for images in the databases. We propose the concept of query verification, which evaluates queries using statistics, and provides users with feedback, including the strictness and reformulation alternatives of each query condition as well as estimated numbers of matches. With query verification, the system increases the efficiency of the multimedia database exploration for both users and the system. Such statistical information is also utilized to support progressive query processing and query relaxation. Received: 9 June 1998/ Accepted: 21 July 2000 Published online: 4 May 2001