SPARE: a development environment for program analysis algorithms

A tool that bridges the gap between the theory and practice of program analysis specifications is described. The tool supports a high-level specification language that enables clear and concise expression of analysis algorithms. The denotational nature of the specifications eases the derivation of formal proofs of correctness for the analysis algorithm. SPARE (structured program analysis refinement environment) is based on a hybrid approach that combines the positive aspects of both the operational and the semantics-driven approach. An extended denotational framework is used to provide specifications in a modular fashion. Several extensions to the traditional denotational specification language have been designed to allow analysis algorithms to be expressed in a clear and concise fashion. This extended framework eases the design of analysis algorithms as well as the derivation of correctness proofs. The tool provides automatic implementation for testing purposes     

From a B formal specification to an executable code: application to the relational database domain

This paper presents a formal approach for the development of trustworthy database applications. This approach consists of three complementary steps. Designers start by modeling applications using UML diagrams dedicated to database applications domain. These diagrams are then automatically translated into B specifications suitable not only for reasoning about data integrity checking but also for the derivation of trustworthy implementations. In this paper, we present a process based on the B refinement technique for the derivation of a SQL relational implementation, embedded in the JAVA language (JAVA/SQL), from a B specification obtained by the first translation phase.     

Parallelization of divide-and-conquer in the Bird-Meertens formalism

An SPMD parallel implementation schema for divide-and-conquer specifications is proposed and derived by formal refinement (transformation) of the specification schema. The specification is in the form of a mutually recursive functional definition. In a first phase, a parallel functional program schema is constructed which consists of a communication tree and a functional program that is shared by all nodes of the tree. The fact that this phase proceeds by semantics-preserving transformations in the Bird-Meertens formalism of higher-order functions guarantees the correctness of the resulting functional implementation. A second phase yields an imperative distributed message-passing implementation of this schema. The derivation process is illustrated with an example: a two-dimensional numerical integration algorithm.Parts of this paper were presented at the International Parallel Processing Symposium, Mexico, 1994 [GoL94] and at the World Transputer Congress, Italy, 1994 [Gor94]     

Translation of Z specifications to executable code: Application to the database domain

ContextIt is well-known that the use of formal methods in the software development process results in high-quality software products. Having specified the software requirements in a formal notation, the question is how they can be transformed into an implementation. There is typically a mismatch between the specification and the implementation, known as the specification-implementation gap.ObjectiveThis paper introduces a set of translation functions to fill the specification-implementation gap in the domain of database applications. We only present the formal definition, not the implementation, of the translation functions.MethodWe chose Z, SQL and Delphi languages to illustrate our methodology. Because the mathematical foundation of Z has many properties in common with SQL, the translation functions from Z to SQL are derived easily. For the translation of Z to Delphi, we extend Delphi libraries to support Z mathematical structures such as sets and tuples. Then, based on these libraries, we derive the translation functions from Z to Delphi. Therefore, we establish a formal relationship between Z specifications and Delphi/SQL code. To prove the soundness of the translation from a Z abstract schema to the Delphi/SQL code, we define a Z design-level schema. We investigate the consistency of the Z abstract schema with the Z design-level schema by using Z refinement rules. Then, by the use of the laws of Morgan refinement calculus, we prove that the Delphi/SQL code refines the Z design-level schema.ResultsThe proposed approach can be used to build the correct prototype of a database application from its specification. This prototype can be evolved, or may be used to validate the software requirements specification against user requirements.ConclusionTherefore, the work presented in this paper reduces the overall cost of the development of database applications because early validation reveals requirement errors sooner in the software development cycle.     

Verifying Contextual Refinement with Ownership Transfer

Contextual refinement is a compositional approach to compositional verification of concurrent objects.There has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract specification.However,these program logics for contextual refinement verification cannot support objects with resource ownership transfer,which is a common pattern in many concurrent objects,such as the memory management module in OS kernels,which transfers the allocated memory block between the object and clients.In this paper,we propose a new approach to give abstract and implementation independent specifications to concurrent objects with ownership transfer.We also design a program logic to verify contextual refinement of concurrent objects w.r.t.their abstract specifications.We have successfully applied our logic to verifying an implementation of the memory management module,where the implementation is an appropriately simplified version of the original version from a real-world preemptive OS kernel.     

面向方面分布式系统形式化规格说明语言

分布式系统复杂性的不断增加以及对可配置性和可重用性要求的不断提高,需要面向方面软件工程方法的支持,而形式化方法能保证分布式系统的正确性。本文对分布式规格说明语言Ocsid进行了面向方面的扩展,讨论了面向方面的Ocsid的框架结构、语法要求、方面的联结和功能接口。定义了面向方面的Ocsid规格说明语言中叠加和组合的形式化描述,该形式化描述覆盖了各个精化阶段,使精化体系的各个独立视点被协调地组合,并能形式化地验证规格说明的时态属性和系统行为。本文的工作针对的是分布式系统的形式化规格说明,提出了面向方面Ocsid的形式基础和方面扩展,其基本思想同样适用于更一般的情况。     

A set‐oriented method definition language for object databases and its semantics

In this paper we propose a set‐oriented rule‐based method definition language for object‐oriented databases. Most existing object‐oriented database systems exploit a general‐purpose imperative object‐oriented programming language as the method definition language. Because methods are written in a general‐purpose imperative language, it is difficult to analyze their properties and to optimize them. Optimization is important when dealing with a large amount of objects as in databases. We therefore believe that the use of an ad hoc, set‐oriented language can offer some advantages, at least at the specification level. In particular, such a language can offer an appropriate framework to reason about method properties. In this paper, besides defining a set‐oriented rule‐based language for method definition, we formally define its semantics, addressing the problems of inconsistency and non‐determinism in set‐oriented updates. Moreover, we characterize some relevant properties of methods, such as conflicts among method specifications in sibling classes and behavioral refinement in subclasses. Copyright © 2003 John Wiley & Sons, Ltd.     

An Implementation of the CORDRA Architecture Enhanced for Systematic Reuse of Learning Objects

The Sharable Content Object Reference Model (SCORM) specification defines metadata of learning objects, which are used as the elementary reusable components in distance learning. The Content Object Repository Discovery And Registration/Resolution Architecture (CORDRA) specification provides a common architecture for the resolution, discovery, and sharing of these learning objects. These two specifications together define standardized ways in which learning objects can be discovered and reused by content designers. However, the current CORDRA and the definition of objects in SCORM only allow an object to be copied, updated, and reorganized in a new content aggregation, which is used as a delivery package to end users. This paper proposes a revised CORDRA architecture and a reusability mechanism to make instruction design easier. In particular, it proposes a structure called a reusability tree for tracking the history of reuse of learning objects in CORDRA. This paper also defines the notions of similarity, diversity, and relevancy of learning objects to make it easier for users to precisely search for and reuse learning objects.     

基于路径无关语言的等价模式演化策略

面向对象数据库的许多应用环境需要频繁的模式演以化,但模式演化以后,基于先前模式的应用程序因此而不得不修改或重编,这就造成了巨大的软件浪费.提出了基于路径无关语言的等价模式演化方案来解决这个问题.首先,路径无关语言是一种面向对象数据库的编程语言,它能使程序脱离对细节数据模式的导航,对模式演化具有较强的适应性.而等价模式演化是一种新的模式演化方案,它能保证用路径无关语言编写的应用程序在模式演化以后无须修改而完全重用.此外,在实现等价模式演化的系统中,为了减少演化开销以及不增加用户的额外编程负担,提出了虚拟关系机制和对象演化技术.     

对象互操作的行为模型

对象互操作表达了一组对象在完成某一任务时的动态协作关系,对象互操作的行为描述与抽象是支持面向对应互操作的基础,对此提出一种活动模型作为描述对象互操作行为的方法,该方法以一阶时态逻辑为基础,表达了互操作对象之间交换消息的时态顺序和不同活动之间的行为关系,在该方法中,提出了活动特化和活动聚合两种行为抽象机制,实现了对象互操作行为的复用,最后讨论了给定论域的类模式和活动模式的一致性集成问题。     

CIMS信息集成平台中的OO视图模型

为了满足ＣＩＭＳ环境中信息集成的要求,本文为信息集成平台设计了一种具有集成功能的面向对象视图模型Ｉ－ＶＩＥＷ．Ｉ－ＶＩＥＷ对ＯＯ模型进行了扩充,定义了虚属性、虚对象的概念;引入了输入与隐藏机制和类派生机制,允许对对象的状态和行为进行提炼,能够很好地解决各类集成问题,如模式映射、评义冲突和模式合并与重构等。     

Object modelling and formal specification during real-time system development

Object oriented techniques promote understanding of requirements leading to flexible and extendible designs. The use of formal specification techniques ensures a complete understanding of system requirements and provides sound foundations for subsequent testing and verification. This paper describes the use of the Z and Timed CSP formal specification techniques to support object modelling during real-time system development. Relationships between class attributes are specified within the corresponding Z schemas and inheritance relationships between classes are formally specified using the schema extension mechanism of Z. Z is used to specify the domain types of the attributes of classes identified during object oriented analysis and design. Z is also used to produce model based specifications of the methods within classes that are specified informally during functional analysis. Dynamic analysis identifies events, states and temporal relationships between events. Timed CSP is used to formally specify this information as well as timing information that is necessary during real-time system development.     

A theory-based representation for object-oriented domain models

Formal software specification has long been touted as a way to increase the quality and reliability of software; however, it remains an intricate, manually intensive activity. An alternative to using formal specifications directly is to translate graphically based, semiformal specifications into formal specifications. However, before this translation can take place, a formal definition of basic object oriented concepts must be found. The paper presents an algebraic model of object orientation that defines how object oriented concepts can be represented algebraically using an object oriented algebraic specification language O-SLANG. O-SLANG combines basic algebraic specification constructs with category theory operations to capture internal object class structure, as well as relationships between classes     

Constraint analysis: a design process for specifying operations onobjects

A design process for an object-oriented database design environment, known as constraint analysis, is presented. Given the increased level of semantics associated with an object-oriented database schema, constraint analysis makes use of semantics expressed as database constraints to support the flexible specification of propagation actions for operations on objects. Constraints are formally represented using Horn logic. The constraint analysis process then reasons about constraints at design time to help the designer understand the effects of constraints on object manipulation, identifying possible constraint violations as well as design alternatives for handling violations. An advantage of constraint analysis is that both inherent and explicit schema constraints are included in the analysis process. A formal representation is given that supports the analysis of constraints and the automatic identification of design alternatives for responding to constraint violations     

Structural Refinement of Systems Specified in Object-Z and CSP

This paper is concerned with methods for refinement of specifications written using a combination of Object-Z and CSP. Such a combination has proved to be a suitable vehicle for specifying complex systems which involve state and behaviour, and several proposals exist for integrating these two languages. The basis of the integration in this paper is a semantics of Object-Z classes identical to CSP processes. This allows classes specified in Object-Z to be combined using CSP operators. It has been shown that this semantic model allows state-based refinement relations to be used on the Object-Z components in an integrated Object-Z/CSP specification. However, the current refinement methodology does not allow the structure of a specification to be changed in a refinement, whereas a full methodology would, for example, allow concurrency to be introduced during the development life-cycle. In this paper, we tackle these concerns and discuss refinements of specifications written using Object-Z and CSP where we change the structure of the specification when performing the refinement. In particular, we develop a set of structural simulation rules which allow single components to be refined to more complex specifications involving CSP operators. The soundness of these rules is verified against the common semantic model and they are illustrated via a number of examples.     

Object oriented concepts identification from formal B specifications

This paper addresses the graphical representation of static aspects of B specifications, using UML class diagrams. These diagrams can help understand the specification for stakeholders who are not familiar with the B method, such as customers or certification authorities. The paper first discusses some rules for a preliminary derivation of a class diagram. It then studies the consistency of the concepts preliminarily identified from an object oriented point of view. A formal concept analysis technique is used to distinguish between consistent classes, attributes, associations and operations. The proposed technique is to incrementally add operations to the formal specification which automatically result in evolutions of the class diagram.     

基于角色的设计模式形式建模及演化

重用设计在改善软件开发过程中的作用越来越受到人们的重视.面向对象的软件设计模式概念的提出为软件设计的重用打开了新的局面.但在设计模式的具体应用中存在实现、文档和组合的问题.给出了一种基于角色的设计模式形式建模方法,将类、类属性、类之间的关系等都看作角色,并用形式建模语言Object-Z形式表示这些角色,可有效地解决设计模式实例化时存在的问题.基于角色的设计模式形式模型在演化时也基于角色进行演化,将模式的演化分为角色层演化和模式层演化,模式层演化是由多个角色层演化组成的.演化后的模型可以通过定理证明器验证与前模型是否保持一致.     

Improving the predictable assembly of service-oriented architectures

Object technology's development and wide adoption has improved software applications' modularity, extensibility, and reusability. An approach that's complementary to OO software reuse entails using "Web services and service-oriented architectures". We propose an intermediate approach to Web service specification. Our technique integrates the use of regular expressions in WSDL specifications to constrain the format of argument and return values to and from Web services. This approach provides the basis for automating the generation of both client- and server-side checking wrappers. The service-oriented paradigm is founded on an assumption of well-specified and well-understood contracts that isn't realized in practice. Our approach extends the WSDL specification language with support for argument- and return-format specification brings us one step closer to realizing the assumptions on which the paradigm is based. This work is important in reducing the adoption barriers that have slowed the acceptance of Web services and SOAs. This is especially important as we closer to realizing the vision of ubiquitous computing that promises transparent integration of widely distributed services.