Search

This paper contributes a technique that expands the set of object invariants that one can reason about in modular verification. The technique uses history invariants, two-state invariants that describe the evolution of data values. The technique enables a flexible new way to specify and verify variations of the observer pattern, including iterators. The paper details history invariants and the new kind of object invariants, and proves a soundness theorem. [ABSTRACT FROM AUTHOR]

Service orientation and enterprise integration has brought new requirements for information systems development processes and methods. Enterprise level service oriented architecture requires a requirement engineering approach, which takes the roles and boundaries between systems and organizations into an account. This paper describes a new way of using UML use cases in systems development projects involving integration and services between systems. The technique, Integration Use Cases, emphasizes the role of intermediate systems (such as service buses), but can be used for modeling point-to-point integration as well. The technique has been created as a response to experienced problems in real world systems development projects and tested in practice in large-scale systems development. The paper introduces the technique and provides examples and experiences from practice. [ABSTRACT FROM AUTHOR]

Despite the importance of capturing a precise and complete set of requirements in the requirements engineering stage, there are few tools that adequately support requirements analysis in the process of capturing quality related requirements (non-functional requirements). This paper presents ElicitO, a requirements elicitation tool aimed at empowering requirements analysts with a knowledge repository that helps in the process of capturing precise non-functional requirements (NFRs) specifications during elicitation interviews. The approach is based on the application of functional and non-functional domain ontologies (quality ontologies) to underpin the elicitation activities. The tool is used as a memory aid to structure elicitation interviews, guide requirements analysts with regard to the important quality aspects relating to a class of applications, and support the development of precise requirements based on characteristics and metrics available in quality model standards. [ABSTRACT FROM AUTHOR]

The research presented in this paper investigates how observation of information- and communication-intensive work in hospital wards can be used to produce requirements for mobile clinical information systems. Over a number of years, we have explored how important properties of clinical situations can be captured through structured observations of actors, processes, and systems. In the paper, we present experience from four observational studies of a total of more than 400 hours in hospital wards. Based on the observational studies, we propose a framework for structured, tomographic, observation of clinical work practice. We also briefly discuss and illustrate how the field data can be analyzed and used as input to the requirements engineering process. [ABSTRACT FROM AUTHOR]

In this paper, we present the methodology and architecture of the natural language processing integration into all stages of the information systems development. We show that if the IS textual documentation is preprocessed and integrated into the business knowledge base development then the whole information systems modeling process can be speeded and improved. Self-organizing map received from information systems documentation and the formal concept analysis are suggested to test the IS documentation comprehensibility and reusability. IBM's Information Framework (IFW) Financial Services Data Model (FSDM) has been used for the present research. By using FSDM we demonstrate that the IS model can be partially recreated from IS textual documents by combining techniques based on self-organizing map and formal concept analysis. Finally the numerical experiment is provided to show that IS documents supplemented with the suggested techniques can be reused in natural language interfaces and save the resources and time needed to develop such interfaces. [ABSTRACT FROM AUTHOR]

Usability evaluation methods are a battery of techniques for assessing the usability of interactive systems or of proposed interactive systems. This paper describes a new evaluation method, particularly appropriate for evaluating safety critical and high quality user interfaces. The method can also be used for informing HCI research. The method is applied when a specification is available of an interactive system, or when a system (or prototype) is working. [ABSTRACT FROM AUTHOR]

This paper claims that the design and construction of safety critical interactive systems require both a task centred approach to support efficiently operator's goals and activities and a system centred approach to increase the dependability of the system. The approach presented proposes a model-based approach integrating tasks and system models. This integration is done at the model level (in a similar way as in [13]) and at the tool level exploiting PetShop environment [3] for the system side and AMBOSS [1] for the task side. The tool level integration describes three different protocols each of them having advantages and limitations. The model-based approaches are introduced through a case study in the field of command and control systems. The application called AGENDA allows operators to define and organize work plan for satellite ground systems. [ABSTRACT FROM AUTHOR]

Probabilistic correctness is an important aspect of reliable systems. A soft real-time system, for instance, may be designed to tolerate some degree of deadline misses under a threshold. Since probabilistic systems may behave differently from their probabilistic models depending on their current environments, checking the systems at runtime can provide another level of assurance for their probabilistic correctness. This paper presents a statistical runtime verification for probabilistic properties using statistical analysis. However, while this statistical analysis collects a number of execution paths as samples to check probabilistic properties within some certain error bounds, runtime verification can only produce one single sample. This paper provides a technique to produce such a number of samples and applies this methodology to check probabilistic properties in wireless sensor network applications. [ABSTRACT FROM AUTHOR]

This paper describes an approach to generate AspectJ aspects from formal specifications written for the Monitoring and Checking (MaC) runtime verification tool. The aspects can serve as the foundation for instrumentation of programs that can be verified at runtime. To demonstrate the practicability of the proposed approach, the authors used a benchmark from the MaC research. The benchmark is based on a safety-critical railroad crossing system comprised of a train, a gate, and a controller. Finally, the paper describes the results from generating Java-MaCs specification scripts to AspectJ aspects, and it compares the proposed approach to related approaches and ones that use aspects. [ABSTRACT FROM AUTHOR]

HALO is a novel aspect language introducing a logic-based pointcut language which combines history-based pointcuts and "escape" conditions for interacting with the base language. This combination is difficult to support when escape conditions access context exposed by "future" join points. This paper introduces a weaving mechanism based on copying objects for resolving such pointcuts. Though this seems a memory consuming solution, it can be easily combined with HALO's analysis for reducing the join point history. Furthermore, pointcuts with escape conditions accessing future join point context, sometimes require less memory than pointcuts that don't, but otherwise implement the same functionality. In this paper, we illustrate this by measuring memory usage for simulations of an e-commerce application, switching between an implementation where the pointcut definitions contain escape conditions referring to future join point context, and an equivalent implementation that doesn't. [ABSTRACT FROM AUTHOR]

This paper focuses on how we can engineer systems so that they can meet their timing requirements. Four separate, but related, issues are addressed: a time band model that caters for the broad set of granularities found in a typical complex system, the delay and deadline statements that allow timing requirements to be specified, scheduling analysis that enables a set of concurrent deadlines to be verified and timing analysis that enables sequential code to be inspected to determine its worst case behaviour. These four topics together with a number of other techniques and tool described in the paper allow real-time behaviour to be delivered. [ABSTRACT FROM AUTHOR]

Boolean Algebra with Presburger Arithmetic (BAPA) is a decidable logic that combines 1) Boolean algebra of sets of uninterpreted elements (BA) and 2) Presburger arithmetic (PA). BAPA can express relationships between integer variables and cardinalities of unbounded sets. In combination with other decision procedures and theorem provers, BAPA is useful for automatically verifying quantitative properties of data structures. This paper examines QFBAPA, the quantifier-free fragment of BAPA. The computational complexity of QFBAPA satisfiability was previously unknown; previous QFBAPA algorithms have non-deterministic exponential time complexity due to an explosion in the number of introduced integer variables. This paper shows, for the first time, how to avoid such exponential explosion. We present an algorithm for checking satisfiability of QFBAPA formulas by reducing them to formulas of quantifier-free PA, with only O(n log(n)) increase in formula size. We prove the correctness of our algorithm using a theorem about sparse solutions of integer linear programming problems. This is the first proof that QFBAPA satisfiability is in NP and therefore NP-complete. We implemented our algorithm in the context of the Jahob verification system. Our preliminary experiments suggest that our algorithm, although not necessarily better for proving formula unsatisfiability, is more effective in detecting formula satisfiability than previous approaches. [ABSTRACT FROM AUTHOR]

Continuous probability distributions are widely used to mathematically describe random phenomena in engineering and physical sciences. In this paper, we present a methodology that can be used to formalize any continuous random variable for which the inverse of the cumulative distribution function can be expressed in a closed mathematical form. Our methodology is primarily based on the Standard Uniform random variable, the classical cumulative distribution function properties and the Inverse Transform method. The paper includes the higher-order-logic formalization details of these three components in the HOL theorem prover. To illustrate the practical effectiveness of the proposed methodology, we present the formalization of Exponential, Uniform, Rayleigh and Triangular random variables. [ABSTRACT FROM AUTHOR]

cminor is a mid-level imperative programming language; there are proved-correct optimizing compilers from C to cminor and from cminor to machine language. We have redesigned cminor so that it is suitable for Hoare Logic reasoning and we have designed a Separation Logic for cminor. In this paper, we give a small-step semantics (instead of the big-step of the proved-correct compiler) that is motivated by the need to support future concurrent extensions. We detail a machine-checked proof of soundness of our Separation Logic. This is the first large-scale machine-checked proof of a Separation Logic w.r.t. a small-step semantics. The work presented in this paper has been carried out in the Coq proof assistant. It is a first step towards an environment in which concurrent cminor programs can be verified using Separation Logic and also compiled by a proved-correct compiler with formal end-to-end correctness guarantees. [ABSTRACT FROM AUTHOR]

One of the most exciting and promising approaches to ensure the correctness of critical systems is software model checking, which considers real code, written with standard programming languages like C. One general technique to implement this approach is producing a reduced model of the software in order to employ existing and efficient tools, like spin. This paper presents the application of the technique to avionics software constructed on top of an application interface (api) compliant with the arinc 653 specification (apex), which is widely employed by the manufacturers in the avionics industry. The paper uses techniques to automatically extract promela models from C source code. These techniques were previously developed by the authors. However, they are now extended to deal with new problems, like real-time aspects and apex scheduling. In order to close the extracted model during the verification, we built a reusable apex-specific environment. This apex environment models the execution engine (i.e. an apex compliant RTOS) that implements apex services. Finally, this paper also contains a novel testing method to ensure the correctness of this apex environment. This testing method uses spin to execute official arinc 653 test cases. [ABSTRACT FROM AUTHOR]

In this paper we define a formal framework to test implementations that can be represented by the class of finite state machines introduced in [10]. First, we introduce an appropriate notion of test. Next, we provide an algorithm to derive test suites from specifications such that the constructed test suites are sound and complete with respect to two of the conformance relations introduced in [10]. In fact, the current paper together with [10] constitute a complete formal theory to specify and test the class of systems covered by the before mentioned stochastic finite state machines. [ABSTRACT FROM AUTHOR]

The characterization and the canonical representation of order n phase type distributions (PH(n)) is an open research problem. This problem is solved for n = 2, since the equivalence of the acyclic and the general PH distributions has been proven for a long time. However, no canonical representations have been introduced for the general PH distribution class so far for n > 2. In this paper we summarize the related results for n = 3. Starting from these results we recommend a canonical representation of the PH(3) class and present a transformation procedure to obtain the canonical representation based on any (not only Markovian) vector-matrix representation of the distribution. Using this canonical transformation method we evaluate the moment bounds of the PH(3) distribution set and present the results of our numerical investigations. [ABSTRACT FROM AUTHOR]

These days, parallel and distributed state-space generation algorithms allow us to generate Markov chains with hundreds of millions of states. In order to solve such Markov chains for their steady-state behaviour, we typically use iterative algorithms, either on a single machine, or on a cluster of workstations. When dealing with such huge Markov chains, the accuracy of the computed probability vectors becomes a critical issue. In this paper we report on experimental studies of, among others, the impact of different iterative solution techniques, erratic and stagnating convergence, the impact of the state-space ordering, the influence of the processor architecture chosen and the accuracy of the measure of interest, in relation to the accuracy of the individual state probabilities. To say the least, the paper shows that the results from analysing extremely large Markov chains should be "appreciated with care", and, in fact, questions the feasibility of the ambitious "5 nines programs" that some companies have recently started. [ABSTRACT FROM AUTHOR]

This paper explores the concept of locality in proofs of global safety properties of asynchronously composed, multi-process programs. Model checking on the full state space is often infeasible due to state explosion. A local proof, in contrast, is a collection of per-process invariants, which together imply the global safety property. Local proofs can be compact: but a central problem is that local reasoning is incomplete. In this paper, we present a "completion" algorithm, which gradually exposes facts about the internal state of components, until either a local proof or a real error is discovered. Experiments show that local reasoning can have significantly better performance over a reachability computation. Moreover, for some parameterized protocols, a local proof can be used to show correctness for all instances. [ABSTRACT FROM AUTHOR]

Software components and software architectures have emerged as a promising paradigm to improve the construction of software systems. Some attributes, such as reliability, requires evidences about failures in the system. An approach addressing the software reliability estimation problem is based on considering all execution traces collected during the testing process. An execution trace is a sequence of blocks grouping source code statements. Following this approach, early reliability assessment of component assemblies requires addressing an important issue: a precise composition semantics representing the behavior of the assembled components. This paper describes a composition model for sequential component assemblies which uses as basic units of composition a set of empirical evidences generated during the component testing process. These units are named as Component Test Records. [ABSTRACT FROM AUTHOR]

In this paper, we extend past work on Linear Scan register allocation, and propose two Extended Linear Scan (ELS) algorithms that retain the compile-time efficiency of past Linear Scan algorithms while delivering performance that can match or surpass that of Graph Coloring. Specifically, this paper makes the following contributions: - We highlight three fundamental theoretical limitations in using Graph Coloring as a foundation for global register allocation, and introduce a basic Extended Linear Scan algorithm, ELS0, which addresses all three limitations for the problem of Spill-Free Register Allocation. - We introduce the ELS1 algorithm which extends ELS0 to obtain a greedy algorithm for the problem of Register Allocation with Total Spills. - Finally, we present experimental results to compare the Graph Coloring and Extended Linear Scan algorithms. Our results show that the compile-time speedups for ELS1 relative to GC were significant, and varied from 15× to 68×. In addition, the resulting execution time improved by up to 5.8%, with an average improvement of 2.3%. Together, these results show that Extended Linear Scan is promising as an alternate foundation for global register allocation, compared to Graph Coloring, due to its compile-time scalability without loss of execution time performance. [ABSTRACT FROM AUTHOR]

This paper presents a way to contract timed STGs effectively for a decomposition based logic synthesis of timed circuits. In the decomposition based synthesis method, a sufficient input signal set for each output is first obtained, and the timed STG is contracted to include only transitions on this input signal set and the output of interest, from which the circuit for the output is synthesized. Care is, however, needed for the contraction of timed STGs. A simple contraction algorithm used for the untimed version can result in the loss of important timing information, causing it to synthesize non-optimal circuits. On the other hand, exact contraction that preserves the timing information precisely is applied only to a small class of transitions, which degrades the performance of the decomposition based synthesis method. This paper proposes a way to contract timed STGs effectively without losing the optimality of the synthesized circuits, and shows some experimental results. [ABSTRACT FROM AUTHOR]

This paper presents an assertional-style verification of the aircraft landing protocol of NASA's SATS (Small Aircraft Transportation System) concept [1] using the I/O automata framework and the PVS theorem prover. We reconstructed the mathematical model of the landing protocol presented in [2] as an I/O automaton. In addition, we translated the I/O automaton into a corresponding PVS specification, and conducted a verification of the safety properties of the protocol using the assertional proof technique and the PVS theorem prover. [ABSTRACT FROM AUTHOR]

The static determination of approximated values of string expressions has many potential applications. For instance, approximated string values may be used to check the validity and security of generated strings, as well as to collect the useful string properties. Previous string analysis efforts have been focused primarily on the maxmization of the precision of regular approximations of strings. These methods have not been completely satisfactory due to the difficulties in dealing with heap variables and context sensitivity. In this paper, we present an abstract-interpretation-based solution that employs a heuristic widening method. The presented solution is implemented and compared to JSA. In most cases, our solution gives results as precise as those produced by previous methods, and it makes the additional contribution of easily dealing with heap variables and context sensitivity in a very natural way. We anticipate the employment of our method in practical applications. [ABSTRACT FROM AUTHOR]

This paper tackles a problem often overlooked in functional programming community: that of testing. Fully automatic test tools like ${\sf{Quickcheck}}$ and ${\sf {G{\forall}ST}}$ can test first order functions successfully. Higher order functions, HOFs, are an essential and distinguishing part of functional languages. Testing HOFs automatically is still troublesome since it requires the generation of functions as test argument for the HOF to be tested. Also the functions that are the result of the higher order function needs to be identified. If a counter example is found, the generated and resulting functions should be printed, but that is impossible in most functional programming languages. Yet, bugs in HOFs do occur and are usually more subtle due to the high abstraction level. In this paper we present an effective and efficient technique to test higher order functions by using intermediate data types. Such a data type mimics and controls the structure of the function to be generated. A simple additional function transforms this data structure to the function needed. We use a continuation based parser library as main example of the tests. Our automatic testing method for HOFs reveals errors in the library that was used for a couple of years without problems. [ABSTRACT FROM AUTHOR]

Randomized algorithms are widely used either for finding efficiently approximated solutions to complex problems, for instance primality testing, or for obtaining good average behavior, for instance in distributed computing. Proving properties of such algorithms requires subtle reasoning both on algorithmic and probabilistic aspects of the programs. Providing tools for the mechanization of reasoning is consequently an important issue. Our paper presents a new method for proving properties of randomized algorithms in a proof assistant based on higher-order logic. It is based on the monadic interpretation of randomized programs as probabilistic distribution [1]. It does not require the definition of an operational semantics for the language nor the development of a complex formalization of measure theory, but only use functionals and algebraic properties of the unit interval. Using this model, we show the validity of general rules for estimating the probability for a randomized algorithm to satisfy certain properties, in particular in the case of general recursive functions. We apply this theory for formally proving a program implementing a Bernoulli distribution from a coin flip and the termination of a random walk. All the theories and results presented in this paper have been fully formalized and proved in the Coq proof assistant [2]. [ABSTRACT FROM AUTHOR]

A common problem with long-lived large industrial software systems such as telecom and industrial automation systems is the increasing complexity and the lack of formal models enabling efficient analyses of critical properties. New features are added or changed during the system life cycle and it becomes harder and harder to predict the impact of maintenance operations such as adding new features or fixing bugs. We present a framework for introducing analyzability in a late phase of the system's life cycle. The framework is based on the general idea of introducing a probabilistic formal model that is analyzable with respect to the system properties in focus, timing and usage of logical resources. The analyses are based on simulations. Traditional analysis method falls short due to a too limited modelling language or problems to scale up to real industrial systems. This method can be used for predicting the impact caused by e.g. adding a new feature or other changes to the system. This enables the system developers to identify potential problems with their design at an early stage and thus decreasing the maintenance cost. The framework primarily targets large industrial real-time systems, but it is applicable on a wide range of software system where complexity is an issue. This paper presents the general ideas of the framework, how to construct, validate, and use this type of models, and how the industry can benefit from this. The paper also present a set of tools developed to support the framework and our experiences from deploying parts of the framework at a company. [ABSTRACT FROM AUTHOR]

Symbolic software verification engines such as Slam and ESC/Java often use automatic theorem provers to implement forms of symbolic simulation. The theorem provers that are used, such as Simplify, usually combine decision procedures for the theories of uninterpreted functions, linear arithmetic, and sometimes bit vectors using techniques proposed by Nelson-Oppen or Shostak. Programming language constructs such as pointers, structures and unions are not directly supported by the provers, and are often encoded imprecisely using axioms and uninterpreted functions. In this paper we describe a more direct and accurate approach towards providing symbolic infrastructure for program verification engines. We propose the use of a theorem prover called Cogent, which provides better accuracy for ANSI-C expressions with the possibility of nested logic quantifiers. The prover's implementation is based on a machine-level interpretation of expressions into propositional logic. Cogent's translation allows the program verification tools to better reason about finite machine-level variables, bit operations, structures, unions, references, pointers and pointer arithmetic. This paper also provides experimental evidence that the proposed approach is practical when applied to industrial program verification. [ABSTRACT FROM AUTHOR]

In this paper we introduce RML, which stands for Rule Markup Language and is used for rule-based transformations of XML. With RML the user can define XML wildcard elements, variables containing parts of the XML such as variables for element names or variables for lists of elements. Any XML vocabulary can be combined with RML to define transformations that can be performed by RML tools also discussed in this paper. As an application of RML we show how it can be used to specify semantics for statecharts and class-diagrams in UML models. The static structure is defined in XML and the dynamic behavior of the model is captured with RML. The RML tools then provide an XML-based execution platform for UML models. This approach therefore can be used to simulate and analyze UML models. Keywords: XML, UML, RML, transformation, rules, simulation. [ABSTRACT FROM AUTHOR]

This paper proposes a methodology to analyze graph transformation systems by means of Alloy and its supporting tools. Alloy is a simple structural modeling language, based on first-order logic, that allows the user to produce models of software systems by abstracting their key characteristics. The tools can generate instances of invariants, and check properties of models, on user-constrained representations of the world under analysis. The paper describes how to render a graph transformation system —specified using AGG— as an Alloy model and how to exploit its tools to prove significant properties of the system. Specifically, it allows the user to decide whether a given configuration (graph) can be obtained through a finite and bounded sequence of steps (invocation of rules), whether a given sequence of rules can be applied on an initial graph, and, given an initial graph and an integer n, which are the configurations that can be obtained by applying a sequence of n (particular) rules. [ABSTRACT FROM AUTHOR]

Graph transformation techniques have already been used successfully by several research groups to support re-engineering of large legacy systems. Where others often aim at transforming the system to improve it, we advocate an evolutionary approach that embeds transformations within the ordinary development process and provides tool support to monitor the ongoing progress regularly. In this paper, we discuss how temporal graph queries based on Fujaba story diagrams can provide a natural means to express trend-oriented metrics and consistency rules that we identified in our industrial case studies. To this end, we discuss a first-order logic rather than operational interpretation of a graph queries and show how well-known temporal logic operators can be added to express rules over consecutive states of the same instance graph. [ABSTRACT FROM AUTHOR]

In unreliable environments, e.g. wireless networks, often there are messages lost, connection and process crashes, among other undesirable fault occurrences. Mechanisms to enhance the dependability of these systems can be employed, but with a performance cost. Analytical approaches are useful to predict performance and dependability values, guiding the system developer to adjust bounds for specific requirements in complex systems. In this paper we use non-functional analysis of Stochastic Object-Based Graph Grammars (SOBGG) models considering classical fault behaviors in distributed systems, allowing the developer to predict performance and dependability values for high performance and resilient systems. The specific contributions of this paper are: (i) revisit the notion of fault representation to allow non-functional analysis, more specifically, steady-state analysis; (ii) discuss the specification of rates associated to SOBGG rules, describing an adequate approach to distributed systems; (iii) show the suitability of the proposed techniques through their application to a case study. Keywords: Object-based graph grammars, distributed systems, fault-tolerance, non-functional analysis, dependability. [ABSTRACT FROM AUTHOR]

The paper presents a case study on the synthesis of labelled transition systems (ltss) for process calculi, choosing as testbed Milner's Calculus of Communicating System (ccs). The proposal is based on a graphical encoding: each ccs process is mapped into a graph equipped with suitable interfaces, such that the denotation is fully abstract with respect to the usual structural congruence. Graphs with interfaces are amenable to the synthesis mechanism based on borrowed contexts (bcs), proposed by Ehrig and König (which are an instance of relative pushouts, originally introduced by Milner and Leifer). The bc mechanism allows the effective construction of an lts that has graphs with interfaces as both states and labels, and such that the associated bisimilarity is automatically a congruence. Our paper focuses on the analysis of the lts distilled by exploiting the encoding of ccs processes: besides offering some technical contributions towards the simplification of the bc mechanism, the key result of our work is the proof that the bisimilarity on processes obtained via bcs coincides with the standard strong bisimilarity for ccs. [ABSTRACT FROM AUTHOR]

A distributed graph (N,D) consists of a network graph N and a commutative diagram D over the scheme N which associates local graphs D(ni) and graph morphisms D(e): D(n1) →D(n2) to nodes n1, n2 and edges e: n1 →n2 in N. Although there are several interesting applications of distributed graphs and transformations, even the basic pushout constructions for the double pushout approach of distributed graph transformation could be shown up to now only in very special cases. In this paper we show that the category of distributed graphs can be considered as a Grothendieck category over a specific indexed category, which assigns to each network N the category of all diagrams D of shape N. In this framework it is possible to give a free construction which allows to construct for each diagram D1 over N1 and network morphism h:N1 →N2 a free extension Fh(D1) over N2 and to show that the Grothendieck category is complete and cocomplete if the underlying category of local graphs has these properties. Moreover, an explicit construction for general pushouts of distributed graphs is given. This pushout construction is based on the free construction. The non-trivial proofs for free constructions and pushouts are the main contributions of this paper and they are compared with the special cases known up to now. [ABSTRACT FROM AUTHOR]

In this paper we describe a way to integrate Taentzer's rule amalgamation with the recently proposed notions of nested graph conditions. The resulting so-called quantified graph transformation rules include (universally and existentially) quantified sub-structures in a flexible way. This can be used for instance to specify a larger-step operational semantics, thus improving the scalability of graph transformation as a technique for software verification. [ABSTRACT FROM AUTHOR]

A service choreography is a model of interactions in which a set of services engage to achieve a goal, seen from the perspective of an ideal observer that records all messages exchanged between these services. Choreographies have been put forward as a starting point for building service-oriented systems since they provide a global picture of the system's behavior. In previous work we presented a language for service choreography modeling targeting the early phases of the development lifecycle. This paper provides an execution semantics for this language in terms of a mapping to π-calculus. This formal semantics provides a basis for analyzing choreographies. The paper reports on experiences using the semantics to detect unreachable interactions. [ABSTRACT FROM AUTHOR]

This paper revolves around the so-called plan revision rules of the agent programming language 3APL. These rules can be viewed as a generalization of procedures. This generalization however results in the semantics of programs of the 3APL language no longer being compositional. This gives rise to problems when trying to define a proof system for the language. In this paper we define a restricted version of plan revision rules which extends procedures, but which does have a compositional semantics, as we will formally show. [ABSTRACT FROM AUTHOR]

This paper describes a multi-agent architecture to support CSCW systems modelling. Since CSCW involves different organizations, it can be seen as a social model. From this point of view, we investigate the possibility of modelling CSCW by agent technology, and then based on organizational semiotics method a multi-agent architecture is proposed via using EDA agent model. We explain the components of this multi-agent architecture and design process. It is argued that this approach provides a new perspective for modelling CSCW systems. Keywords: CSCW, Organizational Semiotics, EDA Agent, Architecture. [ABSTRACT FROM AUTHOR]

In traditional business model, the buying decision process is poorly coordinated among the human decision-makers. Therefore, a long-lived, adaptive, and autonomous application called software agents, that can perform tasks such as personalization, brokering, and negotiation in e-commerce is much needed. These applications reside at the buyers' side or at the sellers' servers. The purpose of this paper is to research into possible deployment of software agents in a framework for e-commerce buying decision process. This paper overviews the traditional business model, the Consumer Buying Behavior (CBB) model, and also covers the requirements needed for minimizing human interactions in buying decision processes. The research proposes a software agent's framework in which, two main approaches, namely Automated Collaborative Filtering (ACF) and Better Business Bureau (BBB), are merged to produce better agents in assisting buying decision process. The framework will enable the agents to get the best price for a good product from a reputable merchant. [ABSTRACT FROM AUTHOR]

There are a lot of services in ubiquitous computing environments. So, ubiquitous service need a service matchmaker which presents more easily and with accuracy. The coupling of webservices and semantic web technology provides the ability to automatically discover, compose and execute webservices. However, the composition of services is generally static because these services are usually described using BPEL4WS or WSFL, restricting dynamic operation because the composite service only has a sequence execution plan. This dynamic composition cannot generate a parallel execution plan for many Internet business applications. In this paper, we design an ontology based framework for dynamic webservice composition. Also, we present a semantic webservice framework using dynamic composition model. This dynamic composition model can generate a parallel execution plan. These plans are calculated using QoS model, hence the best execution plan is selected. [ABSTRACT FROM AUTHOR]

Autonomous agents or semi-autonomous agents feature largely in their dynamic adaptation of its behaviors for changing environments to achieve some set of goals, especially in ubiquitous environments. It demands mechanism for coherently satisfying agent goals depending on changing availability of resources one the fly. Leveraging context-aware techniques and agent-oriented approaches, the paper proposes a lightweight architecture to build adaptive but predictable goal-driven ubiquitous agent systems based on OSGi (Open Service Gateway initiative), an open standard service-oriented framework. The proposed platform not only supports context acquisition, discovery and reasoning, but also provides a centric goal resolution mechanism using goal-tree to automatically specify service components for the satisfaction of agent goals. A Context Pair Language and the production rule are used as semantic basis to model contextual information as well as the goals. [ABSTRACT FROM AUTHOR]

In 3D game contents, the physics engine takes charge of the role to increase the reality of game contents. Objects that act by a decided scenario cause a motion problem for the objects as well as for the reality of the objects. To solve these problems, a physics engine was presented. We proposed a design and implementation of the physics game maker based a physics engine. We also showed the architecture and demo simulation of the physics game maker. This paper explains the basic data structures that compose the physics game maker. We explained the main component that is working in the physics game maker, and showed demo simulation through car simulation. The current physics game maker only processes a rigid body, and supports one world. Keywords: Physics Engine, 3D Game Engine, Game Simulation. [ABSTRACT FROM AUTHOR]

In this paper, we consider an e-Commerce system that supports buying and selling goods or services over the Internet using Mobile Agent(MA) technologies. MAs are active, autonomous, and self-replicable software objects containing both computational logic and state information. When MA technologies are applied to e-Commerce environments, the MAs can search for a product on behalf of the buyer. The buyer constructs a group of MAs, and dispatches each agent in the group to the supplier sites. Each buyer agent compares price information of goods which are suggested by the suppliers. Eventually, all MAs exchange their price information cooperating to determine the most suitable item. In the selection process, if the price information which is exchanged among the MAs is modified by malicious entities, the user may not select intended goods. In this paper, we propose a group session key generation scheme called PGKA(Partial Group session Key Agreement) for secure communication among the MAs. The PGKA has no sponsors, controllers, or any other members charged with special duties. The main idea in PGKA is to distribute the computation of the group session key generation among the members, which makes the scheme suitable for fully distributed environments. In addition, the cost of the key reconstruction is very low in this scheme, because only the seed value is required to be transmitted for the reconstruction process. [ABSTRACT FROM AUTHOR]

To enable efficient and appropriate uses of the resources in web, it is important to provide range query to keep track of the availability and attributes of millions of service which are geographically distributed. Range query in P2P face a performance tradeoff problem between the efficiency of query and number of message: Optimizing one tends to put pressure on the others. In this paper, a range query algorithm had proposed which lookup for every node in range can be done via O(logN) hops, and number of messages is trend to O(logN)+m-1. We evaluate our system in this paper via a simulation and show that its design along with particular Range-query algorithm meets the goals of efficient query and low message load. [ABSTRACT FROM AUTHOR]

Multi-path routing is an important mechanism for Quality of Service of multimedia communication in current networks. The key point of multi-path routing is to develop an efficient method to distribute the traffic over these multiple paths. This paper proposes a novel approach, QMP (QoS Multi-path Routing), to dynamically evolve the traffic distribution parameters using natural computation and make them adaptive to the changes of network flow and topology. First, a kind of function that reflects the changes of the network characteristics is coded using a novel natural computation technique. Then, regarding it as an antibody, QMP uses an artificial immune idea to evolve the function. Using the evolved function, some parameters in the networks can be predicted. After that, this paper proposes a traffic distribution approach that uses the parameters obtained to forward the real-time traffic, and in the meantime, adjusts the traffic parameters to adapt to the new network changes. The simulations show that this approach performs better than the classic optimal routing algorithms on feasibility and is also comparable to the optimal algorithms in terms of performance. Furthermore, QMP is better than the previous excellent multi-path and single-path routing approaches in both aspects of the delays and network resource usage. [ABSTRACT FROM AUTHOR]

Agent based systems are being used to solve problems ranging from Web search strategies to autonomous robots.In this paper we discuss a multi-agent based selfish routing problem in multi-channel wireless mesh networks. In this selfish routing, k pairs of source-sink (destination) pairs are managed by k different intelligent agents. All the agents are selfish; each agent's goal is to minimize its own cost without considering the overall performance of the network. Meanwhile, the agents are rational, they always meet the embarrassment that whether they face the probability of causing interference for routing flow by a short cut or they route flow by a longer way steadily. We introduce the game theoretic tools to direct the agents to make feasible choices. We yield a sufficient condition of the existence of pure strategy Nash equilibria and proof it in this paper (we call this the Strong Transmission Game). Some simulations reveal the feasibility of our proposition. Keywords: Multi-Agent, Wireless Mesh Networks, Game Theory, Nash Equilibrium, Selfish Routing. [ABSTRACT FROM AUTHOR]

This paper presents data grid system based on agent for an efficient interoperability of distributed data. Purpose of the data grid system is an efficient interoperability through sharing and exchanging data among distributed databases. Interoperability of distributed data is a basic condition for cooperation of existing legacy systems. More nodes for cooperation, better for distributed environment. On the other hand, we have to overcome heterogeneous characteristics of data and physical problems of network. Therefore, we use agent system which is independent, autonomous and mobile in distributed platform for solving this problem. As mobile Agent interacts asynchronously, it could lessen network traffic and support workload and distributed processing of services so that it is suitable for data grid system. Also we use XMDR(eXtended Metadata Registry) in ISO/IEC 11179 for sharing and exchanging data and overcome the heterogeneity of data. Therefore we improve availability and transparency of distributed data based on data grid middle- ware using proposed mobile agent and could construct data grid system with low cost. [ABSTRACT FROM AUTHOR]

Mainly concerned with type safety, Featherweight Java, or FJ, is a well known minimal core for Java and Generic Java. However, in the type system of FJ, the treatment of downcast is omitted. In this paper we propose a stronger type system for FJ and FGJ. In order to deal with the cast problems, we introduce some special techniques for types, and also strengthen the types for expressions and methods in terms of the type declaration notations. Supported by the type system and our techniques, we can ensure properties stronger than the ones proved in Igarashi et al's original FJ paper. Examples making the above mentioned contributions clear are illustrated throughout this paper. Furthermore a case study on design patterns showing the advantages of our results is given. Keywords: Featherweight Java, Downcast, Type Safety, Observer Pattern. [ABSTRACT FROM AUTHOR]

Although there are many register allocation algorithms that work well, it can be difficult to correctly implement these algorithms. As a result, it is common for bugs to remain in the register allocator, even after the compiler is released. The register allocator may run, but bugs can cause it to produce incorrect output code. The output program may even execute properly on some test data, but errors can remain. In this paper, we propose novel data flow analyses to statically check that the output code from the register allocator is correct in terms of its data dependences. The approach is accurate, fast, and can identify and report error locations and types. No false alarms are produced. The paper describes our approach, called SARAC, and a tool, called ra-analyzer, that statically checks a register allocation and reports the errors it finds. The tool has an average compile-time overhead of only 8% and a modest average memory overhead of 85KB. [ABSTRACT FROM AUTHOR]

This paper presents planning-based service composition algorithms that dynamically interact with a potentially large-scale directory of service advertisements in order to retrieve matching service advertisements on demand. We start with a simple algorithm for untyped services, similar to a STRIPS planner. This algorithm is refined in two steps, first to exploit type information, and second to support partial type matches. An evaluation confirms that the algorithms scale well with increasing size of the directory and that the support for partial type matches is essential to achieve a low failure rate.The work presented in this paper was partly carried out in the framework of the EPFL Center for Global Computing and supported by the Swiss National Funding Agency OFES as part of the European projects KnowledgeWeb (FP6-507482) and DIP (FP6-507483). Keywords: Service composition, planning, service discovery, semantic web services. [ABSTRACT FROM AUTHOR]