Improved Invariant Generation for Tvoc

The NYU Tvoc project applies the method of translation validation to verify that optimized code is semantically equivalent to the unoptimized code, by establishing, for each run of the optimizing compiler, a set of verification conditions (VCs) whose validity implies the correctness of the optimized run. The core of Tvoc is Tvoc-sp, that handles structure preserving optimizations, i.e., optimizations that do not alter the inner loop structures. The underlying proof rule, Val, on whose soundness Tvoc-sp is based, requires, among other things, to generating invariants at each “cutpoint” of the control graph of both source and target codes. The current implementation of Tvoc-sp employs somewhat naïve fix-point computations to obtain the invariants. In this paper, we propose an alternative method to compute invartiants which is based on simple data-flow analysis techniques.     

Merging the autoview image processing language with prolog

A new computer language, called provision, is defined. It combines features of both prolog (for artificial intelligence) and autoview (for image processing). Predicates for image processing, controlling cameras, illumination sources, optics, a video multiplexor and simple robotic devices are all integrated with PROLOG2, an extension of standard core prolog. The result is a powerful medium for expressing a wide range of algorithms for the visual control of robots and advanced industrial inspection. Several provision applications (i.e. ‘programs’) are presented.     

Nonstandard Analysis in ACL2

ACL2 refers to a mathematical logic based on applicative Common Lisp, as well as to an automated theorem prover for this logic. The numeric system of ACL2 reflects that of Common Lisp, including the rational and complex-rational numbers and excluding the real and complex irrationals. In conjunction with the arithmetic completion axioms, this numeric type system makes it possible to prove the nonexistence of specific irrational numbers, such as 2. This paper describes ACL2(r), a version of ACL2 with support for the real and complex numbers. The modifications are based on nonstandard analysis, which interacts better with the discrete flavor of ACL2 than does traditional analysis.     

Citius altius fortius: Lessons learned from the Theorem Prover Waldmeister

In the last years, the development of automated theorem provers has been advancing in a so to speak Olympic spirit, following the motto “faster, higher, stronger”; and the Waldmeister system has been a part of that endeavour. We will survey the concepts underlying this prover, which implements Knuth-Bendix completion in its unfailing variant. The system architecture is based on a strict separation of active and passive facts, and is realized via specifically tailored representations for each of the central data structures: indexing for the active facts, set-based compression for the passive facts, successor sets for the conjectures. In order to cope with large search spaces, specialized redundancy criteria are employed, and the empirically gained control knowledge is integrated to ease the use of the system. We conclude with a discussion of strengths and weaknesses, and a view of future prospects.     

ReSpecT Nets: Towards an Analysis Methodology for ReSpecT Specifications

A key feature for infrastructures providing coordination services is the ability to define the behaviour of coordination abstractions according to the requirements identified at design-time. We take as a representative for this scenario the logic-based language ReSpecT (Reaction Specification Tuples), used to program the reactive behaviour of tuple centres. ReSpecT specifications are at the core of the engineering methodology underlying the TuCSoN infrastructure, and are therefore the “conceptual place” where formal methods can be fruitfully applied to guarantee relevant system properties.In this paper we introduce ReSpecT nets, a formalism that can be used to describe reactive behaviours that can succeed and fail, and that allows for an encoding to Petri nets with inhibitor arcs. ReSpecT nets are introduced to give a core model to a fragment of the ReSpecT language, and to pave the way for devising an analysis methodology including formal verification of safety and liveness properties. In particular, we provide a semantics to ReSpecT specifications through a mapping to ReSpecT nets. The potential of this approach for the analysis of ReSpecT specifications is discussed, presenting initial results for the analysis of safety properties.     

Synthesis of Optimal Strategies Using HyTech

Priced timed (game) automata extend timed (game) automata with costs on both locations and transitions. The problem of synthesizing an optimal winning strategy for a priced timed game under some hypotheses has been shown decidable in [P. Bouyer, F. Cassez, E. Fleury, and K.G. Larsen. Optimal strategies in priced timed game automata. Research Report BRICS RS-04-4, Denmark, Feb. 2004. Available at http://www.brics.dk/RS/04/4/]. In this paper, we present an algorithm for computing the optimal cost and for synthesizing an optimal strategy in case there exists one. We also describe the implementation of this algorithm with the tool HyTech and present an example.     

Modelling the GSM Handover Protocol in CommUnity

CommUnity is a formal approach to software architecture. It has a precise, yet intuitive mathematical semantics based on category theory. It supports, at the methodological level, a clear separation between computation, coordination, and distribution (including mobility). It provides a simple state-based language for describing component behaviour that is inspired by Unity and Interacting Processes. It also addresses composition as a first class concern and accounts for the emergence of global system properties from interconnections. This paper describes the approach and available tool support by modelling essential aspects of the GSM handover protocol. We also sketch a framework that we are implementing for the distributed execution of such specifications using Klava, a Java library for mobile agent systems based on tuple spaces.     

An algebraic specification of method combination for the Common Lisp Object System

The Common Lisp Object System (CLOS) is an extension of Common Lisp for object-oriented programming being designed as part of the ANSI X3J13 Common Lisp standardization process. This report describes an algebraic specification of the method combination and application component of CLOS. The specification is based on a draft of the standard presented to the ANSI committee in spring of 1987, and was done using an executable, typed functional programming language called Axis. The result suggests a logical mapping from the abstract data types and operations in the specification to the classes and methods which could become that part of the CLOS kernel (called the metaobject protocol) involved in method combination. In addition, the existence of a formal algebraic specification for CLOS allows the effects of changes in the language to be tested during the design phase, rather than during implementation. This is illustrated by showing how the language semantics change when thecall-next-method function is allowed to take arguments, an extension proposed in the draft standard. Standardization documents like the CLOS standard are usually written in a semi-natural language, but if they are accompanied by an additional formal specifiction during their generation, the probability of undetected or lately discovered errors in the design decreases, and the specification also provides an unambiguous source of reference for implementors.     

Rule-Based Programming with Diaplan

Diaplan is a language for programming with graphs and diagrams that is currently being designed and implemented by the authors. In this paper, a programming example, declaration grids, shall illustrate how Diaplan supports a functional and object-oriented style of programming. The example also indicates which features are needed beyond those discussed in previous work on the language [B. Hoffmann, Abstraction and control for shapely nested graph transformation, Fundamenta Informaticae 58 (2003) 39–56].     

OntoTrack: A semantic approach for ontology authoring

OntoTrackis an ontology authoring tool that combines a graph-based hierarchical layout and instant reasoning feedback within one single view. Currently OntoTrack can handle ontologies with an expressivity almost comparable to OWL Lite. The graphical representation provides an animated and zoomable subsumption graph with context sensitive features such as click-able miniature branches or selective detail views, together with drag-and-drop editing. Each editing step is instantly synchronised with an external reasoner in order to provide appropriate graphical feedback about relevant modeling consequences. A recent extention of OntoTrack provides an on-demand textual explanation for subsumption relationships between classes. This paper describes the key features of the current implementation and discusses future work, as well as some development issues. OntoTrack can be downloaded at http://www.informatik.uni-ulm.de/ki/ontotrack/.     

智能对象语言CLOS的分布实现

ＣＬＯＳ系统是一个嵌入Ｃｏｍｍｏｎ Ｌｉｓｐ的面向对象标准语言。文中结合所提出的类分方法，通过引入同步或异步通信协议和ＲＰＣ并发控制，详细介绍了一个新的分布ＣＬＯＳ系统ＰａｒＣＬＯＳ。     

Software specification using the special language

This paper presents a tutorial overview of special, a formal specification and assertion language created by SRI International as part of their hierarchical design methodology. The language is based on a formal model of system behavior and is supported by language processors that assist in the interactive development of specifications. special is a strongly typed language that models data and programs as abstract resources known as objects. Collections of modules known as abstract machines are the major building blocks of a software specification in special. The technical foundations of special and the components of a special specification are described. A sample specification is detailed in an appendix.     

Efficiency issues in the kbmag procedure

A well-known computational approach to finite presentations of infinite groups is the kbmag procedure of Epstein, Holt and Rees. We describe some efficiency issues relating to the procedure and detail two asymptotic improvements: an index for the rewriting system that uses generalized suffix trees and the use of dynamic programming to reduce the number of verification steps.     

Formal ReSpecT in the A&A Perspective

Coordination models and languages have found a new course in the context of MAS (multiagent systems). By re-interpreting results in terms of agent-oriented abstractions, new conceptual spaces are found, which extend the reach of coordination techniques far beyond their original scope. This is for instance the case of coordination media, when recasted in terms of coordination artifacts in the MAS context.In this paper, we take the well-established ReSpecT language for programming tuple centre behaviour, and adopt the A&A (agents and artifacts) meta-model as a perspective to reinterpret, revise, extend and complete it. A formal model of the so-called A&A ReSpecT language is presented, along with an example illustrating its use for MAS coordination.     

Mobile data collection in sensor networks: The TinyLime middleware

In this paper we describe TinyLime, a novel middleware for wireless sensor networks that departs from the traditional setting where sensor data is collected by a central monitoring station, and enables instead multiple mobile monitoring stations to access the sensors in their proximity and share the collected data through wireless links. This intrinsically context-aware setting is demanded by applications where the sensors are sparse and possibly isolated, and where on-site, location-dependent data collection is required. An extension of the Lime middleware for mobile ad hoc networks, TinyLime makes sensor data available through a tuple space interface, providing the illusion of shared memory between applications and sensors. Data aggregation capabilities and a power-savvy architecture complete the middleware features. The paper presents the model and application programming interface of TinyLime, together with its implementation for the Crossbow MICA2 sensor platform.     

Kanga(ROO): Handling the micro-DST of the BaBar experiment with ROOT

A system based on ROOT for handling the micro-DST of the BaBar experiment is described. The purpose of the Kanga system is to have micro-DST data available in a format well suited for data distribution within a world-wide collaboration with many small sites. The design requirements, implementation and experience in practice after three years of data taking by the BaBar experiment are presented.     

TiReX: Replica-exchange molecular dynamics using Tinker

We present a driver program for performing replica-exchange molecular dynamics simulations with the Tinker package. Parallelization is based on the Message Passing Interface, with every replica assigned to a separate process. The algorithm is not communication intensive, which makes the program suitable for running even on loosely coupled cluster systems. Particular attention is paid to the practical aspects of analyzing the program output.

Program summary

Program title: TiReXCatalogue identifier: AEEK_v1_0Program summary URL:http://cpc.cs.qub.ac.uk/summaries/AEEK_v1_0.htmlProgram obtainable from: CPC Program Library, Queen's University, Belfast, N. IrelandLicensing provisions: Standard CPC licence, http://cpc.cs.qub.ac.uk/licence/licence.htmlNo. of lines in distributed program, including test data, etc.: 43 385No. of bytes in distributed program, including test data, etc.: 502 262Distribution format: tar.gzProgramming language: Fortran 90/95Computer: Most UNIX machinesOperating system: LinuxHas the code been vectorized or parallelized?: parallelized with MPIClassification: 16.13External routines: TINKER version 4.2 or 5.0, built as a libraryNature of problem: Replica-exchange molecular dynamics.Solution method: Each replica is assigned to a separate process; temperatures are swapped between replicas at regular time intervals.Running time: The sample run may take up to a few minutes.     

SeCA: A framework for Secure Channel Assignment in wireless mesh networks

To maximize the available throughput in multi-channel multi-radio wireless mesh networks (WMNs), it is a critical issue to design a channel assignment scheme efficiently utilizing orthogonal channels. However, most channel assignment schemes are vulnerable to the misbehaviors of nodes participating in channel assignment, and existing secure channel assignment schemes do not address all of the vulnerabilities. In this paper, we address the threats to channel assignment in WMNs resulting from node misbehaviors and present a generic verification framework to detect such misbehaviors. We develop a concrete verification scheme based on this framework and an existing distributed channel assignment scheme. We validate our approach by implementing the verification scheme and evaluating it through simulation. The results show that our approach improves misbehavior detection with minimum performance overhead.     

GKS in an object-oriented environment

Because of its basis properties, object-oriented programming is well suited to creating user interfaces or graphical applications. However, object-oriented systems are often without graphics or have only a graphical kernel which presents a very low level of use. Besides, such graphical kernels are dependent on the implementation. The use of graphical standards could be an alternative way to bring portability of the applications. Object-oriented systems are often implemented on top of Common Lisp or similar Lisp dialects. In this paper the implementation of an object-oriented shell of an available GKS implementation using an object-oriented extension of Common Lisp will be discussed.     

ChangeLedge: Change design and planning in networked systems based on reuse of knowledge and automation

Proper management of Information Technology (IT) resources and services has become imperative for the success of modern organizations. The IT Infrastructure Library (ITIL) represents, in this context, the most widely accepted framework to help achieve this end. Among the processes that compose ITIL, change management has an important role in defining best practices and processes for the efficient and prompt handling of IT changes. In practice, however, such changes are usually described and documented in an ad hoc fashion, due to the lack of proper support to assist the design process. This hampers knowledge acquired when specifying, planning, and carrying out previous changes to be reused in subsequent requests, even though such reuse may result in fewer incidents and faster specification of change plans. To address this problem, in this paper we present a conceptual solution to support the design and planning of IT changes and explore the concept of change templates as a mechanism to formalize, preserve, and (re)use knowledge in the specification of (recurrent and similar) IT changes. To prove concept and technical feasibility of the proposed solution, we have developed a prototypical implementation of a change management system called ChangeLedge and used it to carry out a set of experiments, considering typical IT changes. The results obtained indicate the effectiveness and efficiency of the system, which is able to generate accurate and actionable change plans in substantially less time than would be spent by a skilled human operator.