Search

System configuration languages are now widely used to drive the deployment and evolution of large computing infrastructures. Most such languages are highly informal, making it difficult to reason about configurations, and introducing an important source of failure. We claim that a more rigorous approach to the development and specification of these languages will help to avoid these difficulties and bring a number of additional benefits. In order to test this claim, we present a formal semantics for the core of the SmartFrog configuration language. We demonstrate how this can be used to prove important properties such as termination of the compilation process. To show that this also contributes to the practical development of clear and correct compilers, we present three independent implementations, and verify their equivalence with each other, and with the semantics. Supported by an extended example from a real configuration scenario, we demonstrate how the process of developing the semantics has improved understanding of the language, highlighted problem areas, and suggested alternative interpretations. This leads us to advocate this approach for the future development of practical configuration languages. [ABSTRACT FROM AUTHOR]

Software design has been well recognized as an important means to achieve high reliability, and formal specification can help enhance the quality of design. However, communications between the designer and the user can become difficult via formal specifications due to the potentially complex mathematical expressions in the specification. This difficulty may lead to the situation where the user may not be closely involved in the process of constructing the specification for quality assurance. To allow formal specification to play more effective roles in software design, we put forward a new approach to deal with this problem in this paper. The approach is characterized by integrating specification animation-based inspection into the process of constructing formal design specifications. We discuss the underlying principle of the approach by explaining how specification animation is utilized as a reading technique for inspection to validate, and then evolve, the current specification towards a satisfactory one. We describe a prototype software tool for the method, and present a case study to show how the method supported by the tool works in practice. [ABSTRACT FROM PUBLISHER]

Today's enterprises demand a high degree of compliance of business processes to meet diverse regulations and legislations. Several industrial studies have shown that compliance management is a daunting task, and organizations are still struggling and spending billions of dollars annually to ensure and prove their compliance. In this paper, we introduce a comprehensive compliance management framework with a main focus on design-time compliance management as a first step towards a preventive lifetime compliance support. The framework enables the automation of compliance-related activities that are amenable to automation, and therefore can significantly reduce the expenditures spent on compliance. It can help experts to carry out their work more efficiently, cut the time spent on tedious manual activities, and reduce potential human errors. An evident candidate compliance activity for automation is the compliance checking, which can be achieved by utilizing formal reasoning and verification techniques. However, formal languages are well known of their complexity as only versed users in mathematical theories and formal logics are able to use and understand them. However, this is generally not the case with business and compliance practitioners. Therefore, in the heart of the compliance management framework, we introduce the Compliance Request Language (CRL), which is formally grounded on temporal logic and enables the abstract pattern-based specification of compliance requirements. CRL constitutes a series of compliance patterns that spans three structural facets of business processes; control flow, employed resources and temporal perspectives. Furthermore, CRL supports the specification of compensations and non-monotonic requirements, which permit the relaxation of some compliance requirements to handle exceptional situations. An integrated tool suite has been developed as an instantiation artefact, and the validation of the approach is undertaken in several directions, which includes internal validity, controlled experiments, and functional testing. [ABSTRACT FROM AUTHOR]

Standards are documents that aim to define norms and common understanding of a subject by a group of people. In order to accomplish this purpose, these documents must define its terms and concepts in a clear and unambiguous way. Standards can be written in two different ways: by informal specification (e.g. natural language) or formal specification (e.g. math-based languages or diagrammatic ones). Remarkable papers have already shown how well-founded ontology languages provide resources for the specification's author to better distinguish concepts and relations meanings, resulting in a better specification. This paper has the objective to expose the importance of truly ontological distinctions for standardizations. To achieve this objective, we evaluate a math-based formal specification, in Z notation, using a well-founded ontology language for a telecommunications case study, the ITU-T Recommendation G.805. The results confirm that truly ontological distinctions are essential for clear and unambiguous specifications. [ABSTRACT FROM AUTHOR]

Wireless sensor and actor networks (WSAN) are captivating significant attention because of their suitability for safety-critical applications. Efficient actor placement in such applications is extremely desirable to perform effective and timely action across the deployment region. Nonetheless, harsh application environment inherently favors random placement of actors that leads to high concentration deployment and strangles coverage. Moreover, most of the published schemes lack rigorous validation and entirely rely on informal techniques (e.g., simulation) for evaluating nonfunctional properties of algorithms. This paper presents a localized movement control actor relocation (MCAR) algorithm that strives to improve connected coverage while minimizing movement overhead. MCAR pursues post-deployment actor repositioning in such a way that actors repel each other for better coverage while staying connected. We employ complementary formal and informal techniques for MCAR verification and validation. We model WSAN as a dynamic graph and transform MCAR to corresponding formal specification using Z notation. The resulting specification is analyzed and validated using Z eves tool. We simulate the specification to quantitatively demonstrate the efficiency of MCAR. Simulation results confirm the efficiency of MCAR in terms of movement overhead and connected coverage compared to contemporary schemes. The results show that MCAR can reduce distance movement up to 32 % while improving coverage up to 29 % compared to published schemes. [ABSTRACT FROM AUTHOR]

Distributed fault localization, isolation and supply restoration (FLISR) algorithm only uses local topology information to improve system reliability in electric power enterprises. It has better adaptability than traditional centralized control architecture. To verify the correctness and reliability of the distributed FLISR algorithm which applied to complex distribution network is very important in the operation of distribution network. A formal method for the specification and verification of the distributed FLISR algorithm which uses linear temporal logic (LTL) language is presented in this paper. In addition, the correctness of the algorithm in interference-free situation and the security of the algorithm in some uncertain interference such as switch action failure, communication failure and other confounding factors are proved mathematically. [ABSTRACT FROM AUTHOR]

The use case point (UCP) method is one of the most commonly used size estimation methods in software development. Applicability of UCP size for the project effort estimation is thoroughly investigated; however, little attention is devoted to the effort estimation of particular task types. The authors have created and cross‐compared prediction models for estimating task‐type efforts by means of UCP size using an Online analytical processing model and R packages on a set of 32 real‐world projects, with the goal of facilitating analysis of the correlation between project sizes and effort required to complete task types. Requirements, scoping, functional specification, and functional testing task types have up to two times better estimation accuracies than project effort. Implementation has slightly better accuracy than the project effort, while the other task types are not correlated to the UCP size. Using estimates of the most correlated task types and other techniques, such as expert judgment for others, we improved the overall project effort prediction accuracy and decreased the error from 26 to 16%. [ABSTRACT FROM AUTHOR]

Non‐functional requirements (NFRs) address important issues in software systems, and are vital in successful software. The NFR problems in a system reflect the complexity of that system. Ideally, NFRs are systematically investigated to determine the aspects that may be harmonious or cause conflicts so that conflicts should be detected as early as possible. The work aims to extend the scopes of the NFRs framework and softgoal interdependency graph (SIG) for modelling and analysing NFRs. A formal ontological approach to modelling NFR interactions is proposed, and a core NFR ontology is developed in the ontology web language. The mechanisms involved in NFR interactions with SIG models (through interdependencies in the softgoals) are investigated and formalised. The NFRs are first analyses using a semantic modelling process to provide evaluation criteria. Next, correlation rules for implicit softgoal interdependencies are proposed from knowledge of the domain, and rules for indirect semantic correlations are proposed by extending the delta evaluation method. Reasonable rules in the semantic web environment are defined to allow conflicts between NFRs in SIG instance models to be detected and analysed. A concepts proof is performed to illustrate tool support of the proposed method, and validate the rules for conflict detection. [ABSTRACT FROM AUTHOR]

We present solutions to the three challenges of the VerifyThis competition held at the 18th FM symposium in August 2012. These solutions use the Why3 environment for deductive program verification. [ABSTRACT FROM AUTHOR]

Fair input/output (or I/O) automata are a state-machine model for specifying and verifying reactive and concurrent systems. For the verification purposes, one is usually interested only in the sequences of interactions fair I/O automata offer to their environment. These sequences are called fair traces. The usual approach to the verification consists in proving fair trace inclusion between fair I/O automata. This paper presents a simple approach to the specification of fair traces and shows how to establish a fair trace inclusion relation for a pair of fair I/O automata by using the temporal logic of actions. [ABSTRACT FROM AUTHOR]

UML-B is a 'UML-like' graphical front-end for Event-B that provides support for object-oriented and state machine modelling concepts, which are not available in Event-B. In particular, UML-B includes class diagram and state machine diagram editors with automatic generation of corresponding Event-B. In Event-B, refinement is used to relate system models at different abstraction levels. The same refinement concepts are also applicable in UML-B but require special consideration due to the higher-level modelling concepts. In previous work, we described a case study to introduce support for refinement in UML-B. We now provide a more complete presentation of the technique of refinement in UML-B including a formalisation of the refinement rules and a definition of the extensions to the abstract syntax of UML-B notation. The provision of gluing invariants to discharge the proof obligations associated with a refinement is a significant step in providing verifiable models. We discuss and compare two approaches for constructing gluing invariants in the context of UML-B refinement. [ABSTRACT FROM AUTHOR]

In computer science, functional orbits – i.e., tracks left by the iterations of a function – in a finite domain naturally appear at a high or a low level. This paper introduces a Coq logical orbit framework, the purpose of which is to help rigorously developing software systems with some complex data structures from specification to implementation. The result is a Coq library of orbit concepts formalized as definitions, lemmas and theorems. Most of them are inspired by our previous work in geometric modelling, where combinatorial hypermaps were used to describe surface subdivisions appearing in computational geometry problems, e.g., building convex hulls or Delaunay diagrams. Now, this domain remains a reference for us, but our results are drastically extended and usable in other computer science areas. The proof of Floyd's cycle-detection algorithm, known as “the tortoise and the hare”, confirms that point. The library contains operations to observe, traverse and update orbits – addition, deletion, mutation, transposition – with proofs of their behavior. It focuses on the important case where the involved function is a partial injection. In this case, it defines a connectivity relationship and evaluates the variation of the number of connected components during updates. [ABSTRACT FROM AUTHOR]

In this paper, we describe research results arising from a technology transfer exercise on agent-oriented requirements engineering with an industry partner. We introduce two improvements to the state-of-the-art in agent-oriented requirements engineering, designed to mitigate two problems experienced by ourselves and our industry partner: (1) the lack of systematic methods for agent-oriented requirements elicitation and modelling; and (2) the lack of prescribed deliverables in agent-oriented requirements engineering. We discuss the application of our new approach to an aircraft turnaround simulator built in conjunction with our industry partner, and show how agent-oriented models can be derived and used to construct a complete requirements package. We evaluate this by having three independent people design and implement prototypes of the aircraft turnaround simulator, and comparing the three prototypes. Our evaluation indicates that our approach is effective at delivering correct, complete, and consistent requirements that satisfy the stakeholders, and can be used in a repeatable manner to produce designs and implementations. We discuss lessons learnt from applying this approach. [ABSTRACT FROM PUBLISHER]

This paper presents a computational method that employs Natural Language Processing (NLP) and text mining techniques to support requirements engineers in extracting and modeling goals from textual documents. We developed a NLP-based goal elicitation approach within the context of KAOS goal-oriented requirements engineering method. The hierarchical relationships among goals are inferred by automatically building taxonomies from extracted goals. We use smart metering system as a case study to investigate the proposed approach. Smart metering system is an important subsystem of the next generation of power systems (smart grids). Goals are extracted by semantically parsing the grammar of goal-related phrases in abstracts of research publications. The results of this case study show that the developed approach is an effective way to model goals for complex systems, and in particular, for the research-intensive complex systems. [ABSTRACT FROM PUBLISHER]

Abstract: We describe one of the first attempts at using modern specification techniques in the field of geometric modeling and computational geometry. Using the Coq system, we developed a formal multi-level specification of combinatorial maps, used to represent subdivisions of geometric manifolds, and then exploited it to formally prove fundamental theorems. In particular, we outline here an original and constructive proof of a combinatorial part of the famous Surface Classification Theorem, based on a set of so-called “conservative” elementary operations on subdivisions. [Copyright &y& Elsevier]

In supervisory control of timed discrete-event systems (TDESs), a conceptually well founded finitary control synthesis framework is developed, and it requires specifications to be prescribed as finite (-trace) automata in the form of timed transition graphs (TTGs). However, prescribing real-time specifications as TTGs is a nontrivial task that must be resolved before the formal framework could expect to become widely used. In addressing this specification problem, metric temporal logic (MTL) is proposed in this paper as a control specification language for use with the TTG-based control synthesis framework. MTL is a designer-friendly formalism due to its human or natural language expressiveness and readability, and is well suited for specifying real-time control specifications. In automating TTG prescription, this paper proposes an MTL interface to the control synthesis framework. The interface is proved to be a correct and complete translation algorithm that converts finitary control specifications written in state-based MTL formulas for a given TDES model into deterministic finite TTGs. Integrated, the MTL interface and the control synthesis framework combine the human expressiveness and readability of MTL with the algorithmic computability of TTGs, and together provide a new and convenient MTL specification-based design tool for automated prescription of TTGs and real-time control synthesis. Illustrative examples demonstrate the utility of the MTL interface. [ABSTRACT FROM AUTHOR]

As ubiquitous computing becomes a reality, its applications are increasingly being used in business-critical, mission-critical and even in safety-critical, areas. Such systems must demonstrate an assured level of correctness. One approach to the exhaustive analysis of the behaviour of systems is formal verification, whereby each important requirement is logically assessed against all possible system behaviours. While formal verification is often used in safety analysis, it has rarely been used in the analysis of deployed pervasive applications. Without such formality it is difficult to establish that the system will exhibit the correct behaviours in response to its inputs and environment. In this paper, we show how model-checking techniques can be applied to analyse the probabilistic behaviour of pervasive systems. As a case study we apply this technique to an existing pervasive message-forwarding system, Scatterbox. Scatterbox incorporates many typical characteristics of pervasive systems, such as dependence on sensor reliability and dependence on context. We assess the dynamic temporal behaviour of the system, including the analysis of probabilistic elements, allowing us to verify formal requirements even in the presence of uncertainty in sensors. We also draw some tentative conclusions concerning the use of formal verification for pervasive computing in general. [ABSTRACT FROM AUTHOR]

Hierarchical part-of relationships/aggregation structures and related queries are essential parts of information systems. However, relational database query languages do not explicitly support hierarchical relationships and queries. A hierarchical query may require a great number of join operations, which increases the effort in query formulation. Therefore, we propose path expressions in formulating hierarchical views over relational data because path expressions are a conventional and compact way to represent hierarchical relationships. We embed path expressions within SQL queries and compile them to standard SQL. This ensures that the path expressions can straightforwardly be implemented on the top of standard relational database systems. The compilation of a path expression is given by an attribute grammar, a conventional formalism to define the semantics of a language. [ABSTRACT FROM PUBLISHER]

Decision-based processes are composed of tasks whose application may depend on explicit decisions relying on the state of the process environment. In specific domains such as healthcare, decision-based processes are often complex and critical in terms of timing and resources. The paper presents a variety of tool-supported techniques for analyzing models of such processes. The analyses allow a variety of errors to be detected early and incrementally on partial models, notably: inadequate decisions resulting from inaccurate or outdated information about the environment state; incomplete decisions; non-deterministic task selections; unreachable tasks along process paths; and violations of non-functional process requirements involving time, resources or costs. The proposed techniques are based on different instantiations of the same generic algorithm that propagates decorations iteratively through the process model. This algorithm in particular allows event-based models to be automatically decorated with state-based invariants. A formal language supporting both event-based and state-based specifications is introduced as a process modeling language to enable such analyses. This language mimics the informal flowcharts commonly used by process stakeholders. It extends High-Level Message Sequence Charts with guards on task-related and environment-related variables. The language provides constructs for specifying task compositions, task refinements, decision trees, multi-agent communication scenarios, and time and resource constraints. The proposed techniques are demonstrated on the incremental building and analysis of a complex model of a real protocol for cancer therapy. [ABSTRACT FROM PUBLISHER]

Formal specification is an active research field in software engineering of this century, where different configurations and techniques are employed and although their industrial use is still limited, the scientific community currently has a different understanding about its usefulness and necessity. Until present time, researchers' work focuses on the specification written during the design of the preliminary functional model, for this reason it mainly focuses on evaluating the related tools. In this paper, a literature review is performed, covering the essence, function, use and disadvantages of formal specification techniques and some assessment and evaluation criteria are analyzed regarding their weaknesses. The results become the basis for future work formulation, aimed to the strengthening of formal specification as a core research activity. [ABSTRACT FROM AUTHOR]

In the real‐world, there are many types of software systems and software engineers always deal with changes. The value of large systems decreases significantly as the requirements and operational environment change over time. Modern software systems are expected to have dynamic reconfigurations to cope with failure and changes. Software adaptation techniques try to overcome the change problem by reconfiguration. In this study, at first, the authors present a formal framework to represent the whole system and then, build a mathematical model called 'adaptor' based on adaptation contract and system architecture. The adaptor is used to define automatic fit between two different components of the system. Finally, for specifying the whole adaptor system the authors will introduce adaptor network using synchronisation vectors. [ABSTRACT FROM AUTHOR]

Creating a formal specification for a design is an error-prone process. At the same time, debugging incorrect specifications is difficult and time consuming. In this work, we propose a debugging method for formal specifications that does not require an implementation. We handle conflicts between a formal specification and the informal design intent using a simulation-based refinement loop, where we reduce the problem of debugging overconstrained specifications to that of debugging unrealizability. We show how model-based diagnosis can be applied to locate an error in an unrealizable specification. The diagnosis algorithm computes properties and signals that can be modified in such a way that the specification becomes realizable, thus pointing out potential error locations. In order to fix the specification, the user must understand the problem. We use counterstrategies to explain conflicts in the specification. Since counterstrategies may be large, we propose several ways to simplify them. First, we compute the counterstrategy not for the original specification but only for an unrealizable core. Second, we use a heuristic to search for a countertrace, i.e., a single input trace which necessarily leads to a specification violation. Finally, we present the countertrace or the counterstrategy as an interactive game against the user, and as a graph summarizing possible plays of this game. We introduce a user-friendly implementation of our debugging method and present experimental results for GR(1) specifications. [ABSTRACT FROM AUTHOR]

The standard hardware design flow involves: (a) design of an integrated circuit using a hardware description language, (b) extensive functional and formal verification, and (c) logical synthesis. However, the above-mentioned processes consume significant effort and time. An alternative approach is to use a formal specification language as a high-level hardware description language and synthesize hardware from formal specifications. Our work is a case study of the synthesis of the widely and industrially used AMBA AHB protocol from formal specifications. Bloem et al. presented the first formal specifications for the AMBA AHB Arbiter and synthesized the AHB Arbiter circuit. However, in the first formal specification some important assumptions were missing. Our contributions are as follows: (a) We present detailed formal specifications for the AHB Arbiter incorporating the missing details, and obtain significant improvements in the synthesis results (both with respect to the number of gates in the synthesized circuit and with respect to the time taken to synthesize the circuit), and (b) we present formal specifications to generate compact circuits for the remaining two main components of AMBA AHB, namely, AHB Master and AHB Slave. Thus with systematic description we are able to automatically and completely synthesize an important and widely used industrial protocol. [ABSTRACT FROM AUTHOR]

Over the last decade, great progress has been made in developing practical transactional memory (TM) implementations, but relatively little attention has been paid to precisely specifying what it means for them to be correct, or formally proving that they are. In this paper, we present TMS1 (Transactional Memory Specification 1), a precise specification of correct behaviour of a TM runtime library. TMS1 targets TM runtimes used to implement transactional features in an unmanaged programming language such as C or C++. In such contexts, even transactions that ultimately abort must observe consistent states of memory; otherwise, unrecoverable errors such as divide-by-zero may occur before a transaction aborts, even in a correct program in which the error would not be possible if transactions were executed atomically. We specify TMS1 precisely using an I/O automaton (IOA). This approach enables us to also model TM implementations using IOAs and to construct fully formal and machine-checked correctness proofs for them using well established proof techniques and tools. We outline key requirements for a TM system. To avoid precluding any implementation that satisfies these requirements, we specify TMS1 to be as general as we can, consistent with these requirements. The cost of such generality is that the condition does not map closely to intuition about common TM implementation techniques, and thus it is difficult to prove that such implementations satisfy the condition. To address this concern, we present TMS2, a more restrictive condition that more closely reflects intuition about common TM implementation techniques. We present a simulation proof that TMS2 implements TMS1, thus showing that to prove that an implementation satisfies TMS1, it suffices to prove that it satisfies TMS2. We have formalised and verified this proof using the PVS specification and verification system. [ABSTRACT FROM AUTHOR]

As software systems are becoming increasingly complex, they need to dynamically and continually adapt their behavior to changing conditions in the long-term running. There will be large numbers of adaptations in these systems when evolving and the adaptations may be unknowable until system operation. To specify these adaptations, this paper proposes the mode-supported Linear Temporal Logic (mLTL) that is an effective way to describe global specifications of adaptive software. The global specifications are defined for adaptive software as requirements from the perspective of global adapting process. The model checking problem of mLTL is also resolved using Linear Temporal Logic (LTL) and Labelled Transition System Analyser (LTSA). Finally, we provide a prototype implementation for modelling and analyzing adaptive programs, and experimental evaluation shows feasibility and scalability of our approach. [ABSTRACT FROM AUTHOR]

An Enterprise JavaBeans (EJB) interceptor is a software mechanism that provides for introducing behaviour implemented as separate code into the execution of a Java application. In this way, EJB interceptors provide a clear separation of the core functionality of the bean and other concerns, such as logging or performance analysis. Despite the beauty of the idea behind the i nterceptors, developing, testing and managing dependencies introduced by the interceptors are considered to be daunting tasks. For example, the developers can specify interceptors at multiple locations and by multiple means. However, different locations and specification means influence the order of the interceptor invocation, which is governed by more than 15 different intertwined rules defined in the EJB standard. To facilitate development of EJB applications, we have designed I2SD, Interceptors to Sequence Diagrams, a tool for reverse engineering EJB applications with interceptors to unified modeling language (UML) sequence diagrams. I2SD provides the developer with a visual feedback and can be used by quality managers to obtain insights in the ways interceptors are used in their project. [ABSTRACT FROM AUTHOR]

A model-based agent system model for medicine usage management is presented and formally analysed. The model incorporates an intelligent ambient agent model that has an explicit representation of a dynamical system model to estimate the medicine level in the patient s body by simulation, is able to analyse whether the patient intends to take the medicine too early or too late, and can take measures to prevent this. [ABSTRACT FROM AUTHOR]

Maintaining inter-actor connectivity is extremely crucial in mission-critical applications of Wireless Sensor and Actor Networks (WSANs), as actors have to quickly plan optimal coordinated responses to detected events. Failure of a critical actor partitions the inter-actor network into disjoint segments besides leaving a coverage hole, and thus hinders the network operation. This paper presents a Partitioning detection and Connectivity Restoration (PCR) algorithm to tolerate critical actor failure. As part of pre-failure planning, PCR determines critical/non-critical actors based on localized information and designates each critical node with an appropriate backup (preferably non-critical). The pre-designated backup detects the failure of its primary actor and initiates a post-failure recovery process that may involve coordinated multi-actor relocation. To prove the correctness, we construct a formal specification of PCR using Z notation. We model WSAN topology as a dynamic graph and transform PCR to corresponding formal specification using Z notation. Formal specification is analyzed and validated using the Z Eves tool. Moreover, we simulate the specification to quantitatively analyze the efficiency of PCR. Simulation results confirm the effectiveness of PCR and the results shown that it outperforms contemporary schemes found in the literature. [ABSTRACT FROM AUTHOR]

Current computer conflict simulation games, or wargames, are opaque in the sense that most of the game mechanisms are not directly visible to the players and are frequently not described in user accessible documentation, have a transient lifetime that is mainly shaped by the evolution of graphics hardware and processor speed, and do not, in contrast with, for example, the well-known abstract board games CHESS and GO, have the technical prerequisites for critical intellectual discussion that the thought-intensive and knowledge-rewarding character of these games seems to warrant. The main reason for this state of affairs is that many of the mechanisms of the games, and in particular the details of how the game state changes over time, are directly expressed in computer code. This is purely a technical problem, and it has a straightforward solution, namely, treating this information as data by creating a formalism for describing not just the game map and playing pieces but also all the game rules including the “sequence of play.” The article suggests such a formalism and shows a complete specification of a simple, but complicated enough for present purposes, “introductory” board wargame. This formalism, with tools that support it, can provide an unambiguous authoritative definition of the rules, accessible by both human and computer players; would allow existing board wargames to be played on a computer, without any simplifications or sacrifices of rule details; and may allow construction of more advanced computer players, since a complete formal specification of the game rules is available as input to them. [ABSTRACT FROM AUTHOR]

Dataspace systems have been proposed recently as an alternative to the traditional data integration approach. They offer reduced setup time and costs by allowing cooperation among the data sources based on the knowledge gained gradually through user interaction. A dataspace is a collection of heterogeneous and beforehand unfamiliar but interrelated data sources. In this article, we consider dataspaces composed of XML-based data sources. The XML query and analysis systems designed to satisfy the user’s sophisticated information needs presuppose that they are familiar with the contents, structures and semantics of the underlying data sources. In order to provide this information, we introduce and specify a schemaless XML dataspace profiling system that assists the user in selecting data sources relevant to him/her and in validating their consistency by detecting the potential data conflicts among them. We also demonstrate how our approach affords the possibility of utilizing an advanced XML query system. [ABSTRACT FROM PUBLISHER]

Runtime verification is a relatively recent area of research that concentrates on checking system execution against formally specified behavioral properties. Primary research directions in runtime verification include logics for monitoring, online checking algorithms, extraction of observations necessary for checking, and reduction of checking overhead. This article gives a brief overview of runtime verification research. [ABSTRACT FROM AUTHOR]

Coverage is a means to quantify the quality of a system specification, and is frequently applied to assess progress in system validation. Coverage is a standard measure in testing, but is very difficult to compute in the context of formal verification. We present efficient algorithms for identifying those parts of the system that are covered by a given property. Our algorithm is integrated into state-of-the-art Boolean satisfiability problem-based model checking using Craig interpolation. The key insight into our algorithm is the re-use of previously computed inductive invariants and counterexamples. This re-use permits a a rapid completion of the vast majority of tests, and enables the computation of a coverage measure with 96% accuracy with only 5× the runtime of the model checker. [ABSTRACT FROM PUBLISHER]

Software inspection is a static analysis technique that is widely used for defect detection, but which suffers from a lack of rigor. In this paper, we address this problem by taking advantage of formal specification and analysis to support a systematic and rigorous inspection method. The aim of the method is to use inspection to determine whether every functional scenario defined in the specification is implemented correctly by a set of program paths and whether every program path of the program contributes to the implementation of some functional scenario in the specification. The method is comprised of five steps: deriving functional scenarios from the specification, deriving paths from the program, linking scenarios to paths, analyzing paths against the corresponding scenarios, and producing an inspection report, and allows for a systematic and automatic generation of a checklist for inspection. We present an example to show how the method can be used, and describe an experiment to evaluate its performance by comparing it to perspective-based reading (PBR). The result shows that our method may be more effective in detecting function-related defects than PBR but slightly less effective in detecting implementation-related defects. We also describe a prototype tool to demonstrate the supportability of the method, and draw some conclusions about our work. [ABSTRACT FROM PUBLISHER]

Current computer conflict simulation games, or wargames, are opaque in the sense that most of the game mechanisms are not directly visible to the players and are frequently not described in user accessible documentation, have a transient lifetime that is mainly shaped by the evolution of graphics hardware and processor speed, and do not, in contrast with, for example, the well-known abstract board games CHESS and GO, have the technical prerequisites for critical intellectual discussion that the thought-intensive and knowledge-rewarding character of these games seems to warrant. The main reason for this state of affairs is that many of the mechanisms of the games, and in particular the details of how the game state changes over time, are directly expressed in computer code. This is purely a technical problem, and it has a straightforward solution, namely, treating this information as data by creating a formalism for describing not just the game map and playing pieces but also all the game rules including the "sequence of play." The article suggests such a formalism and shows a complete specification of a simple, but complicated enough for present purposes, "introductory" board wargame. This formalism, with tools that support it, can provide an unambiguous authoritative definition of the rules, accessible by both human and computer players; would allow existing board wargames to be played on a computer, without any simplifications or sacrifices of rule details; and may allow construction of more advanced computer players, since a complete formal specification of the game rules is available as input to them. [ABSTRACT FROM AUTHOR]

Abstract: We present a formal model to represent orchestrations and choreographies and we define several conformance semantic relations allowing to detect whether a set of orchestration models, representing some web services, leads to the overall communications described in a choreography. Given this formal model, we develop automatic methods to derive a set of web services from a given choreography, in such a way that the system consisting of these services necessarily conforms to the choreography. These methods enable the construction of conforming systems of services even in cases where projecting the choreography into each service would lead to a non-conforming system. This issue is addressed by adding some control messages that make services interact as required by the choreography. Two different derivation methods are presented. In the centralized method, a new service is responsible of managing these additional control messages. In the decentralized method, the responsibility of handling these messages is distributed among all services. [Copyright &y& Elsevier]

This paper discusses the formal validation for spatial information databases integration framework (SIDIF). A SIDIF database is a large, organized body of persistent data, usually associated with computerized software designed to update, query, and retrieve components of the data stored within the system. One of the common difficulties faced by the developer is in designing a robust database system. Even so, in order to solve this matter, developers have to focus their efforts on the formal specifications. The formal specification is supposed to reduce the overall development time. Formal specifications can be used to provide an unambiguous and precise supplement to natural language descriptions. Besides, it can be rigorously validated and verified leading to the early detection of specification errors. Consequently, to validate this problem formally, we specify the SIDIF database framework using Z language and prove by using Z/EVES theorem proven tool. By using this kind of tools, it may help to reduce time, energy and mistake compared to manual theorem proving which can be error task and tedious. [ABSTRACT FROM AUTHOR]

Abstract: We describe the first formal specification of a non-trivial subset of MPI, the dominant communication API in high performance computing. Engineering a formal specification for a non-trivial concurrency API requires the right combination of rigor, executability, and traceability, while also serving as a smooth elaboration of a pre-existing informal specification. It also requires the modularization of reusable specification components to keep the length of the specification in check. Long-lived APIs such as MPI are not usually ‘textbook minimalistic’ because they support a diverse array of applications, a diverse community of users, and have efficient implementations over decades of computing hardware. We choose the TLA+ notation to write our specifications, and describe how we organized the specification of around 200 of the 300 MPI 2.0 functions. We detail a handful of these functions in this paper, and assess our specification with respect to the aforementioned requirements. We close with a description of possible approaches that may help render the act of writing, understanding, and validating the specifications of concurrency APIs much more productive. [Copyright &y& Elsevier]

Writing formal specifications can help developers understand users' requirements, and build a solid foundation for implementation. But like other activities in software development, it is error-prone, especially for large-scale systems. In practice, effective detection of specification errors still remains a challenge. In this paper, we put forward a rigorous, systematic method for the inspection of model-based formal specifications. The method makes good use of the well-defined consistency properties of a specification to provide precise rules and guidelines for inspection. The inspection process utilizes both well-defined expressions derived from the specification and human inspectors' judgments to find errors. We present a case study of the method by describing how it is applied to inspect an Automated Teller Machine (ATM) software specification to investigate the method's feasibility, and explore potential challenges in using it. We also describe a prototype software tool including its functions and distinct features to demonstrate the tool supportability of the method. [ABSTRACT FROM PUBLISHER]

Modern day computer architectures offer ever-increasing support for parallel processing, still it turns out to be quite difficult for programmers and therefore programs to tap into these parallel resources. To benefit from real general-purpose parallel computing we claim that it is likely that a paradigm shift is needed in the way we think about programming. This change of thought in turn will need to be reflected in future programming languages as well. We think that the field of process algebra provides thorough insight in how to reason about the construction of software for concurrent systems and will be one of the enabling technologies supporting this transition. The wish to connect process algebra, a mathematical theory, to the world of computer-readable and executable specifications led to the development of PSF (Process Specification Formalism). PSF is an implementation of the process algebra ACP (Algebra of Communicating Processes) integrating ASF (Algebraic Specification Formalism) to specify algebraic data types. One of the first publications on PSF appeared in Fundamenta Informaticae in 1990. Here we stated as the first sentence of the abstract: "Traditional methods for programming sequential machines are inadequate for specifying parallel systems". Unfortunately, though some advancements have been made since 1990, we can still uphold this statement 20 years later. This current report documents the developments that lead to the construction of PSF and the 1990 publication and moreover it also documents how PSF and its tools have evolved since 1990 taking the conclusion and the outlook for future work from the original article as a reference point. Using the knowledge gained both in constructing tools for PSF and in using PSF to specify concurrent systems, we will judge, discuss and criticise the design decisions taken and show paths for future developments. [ABSTRACT FROM AUTHOR]

Abstract: We report on a method for formally specifying and verifying programmable logic controllers (PLCs) in the specification language TLA+. The specification framework is generic. It separates the description of the environment from that of the controller itself and its structure is consistent with the scan cycle mechanism used by PLCs. Specifications can be parameterized with the number of replicated components. In our experience, the structuring mechanisms of TLA+ help to obtain clear, well-organized, and configurable specifications, finite instances of which are verified by the TLA+ model checker TLC. We have validated our approach on a concrete case study, a controller for fire fighting equipment in a ship dock, and report on the results obtained for this case study. [Copyright &y& Elsevier]

Abstract: The natural immune system is a subject of great research interests because it provides powerful and flexible information processing capability as a decentralized intelligent system. The immune system constitutes an excellent model of adaptive cooperation at the local level and of emergent behaviour at the global level. These concepts can be applied in the Multi-Agent Systems field where autonomous agents interact in order to solve a common goal. There exists several theories to explain immunological phenomena and software models to simulate various components in the immune system. This paper presents a formal specification of the idiotypic network theory viewed as an agent architecture. The specification gives a precise and non ambiguous description of this architecture which is validated through the automatic generation of traces and interesting properties are proven. This specification constitutes a starting point for understanding, reuse and implementations of this architecture. The approach is illustrated with the robot soccer simulation example. [Copyright &y& Elsevier]

Component-based software engineering (CBSE) is viewed as an opportunity to deal with the increasing complexity of modern-day software. Along with CBSE comes the notion of component markets, where more or less generic pieces of software are traded, to be combined into applications by third-party application developers. For such a component market to work successfully, all relevant properties of components must be precisely and formally described. This is especially true for non-functional properties, such as performance, memory foot print, or security. While the specification of functional properties is well understood, non-functional properties are only beginning to become a research focus. This paper discusses semantic concepts for the specification of non-functional properties, taking into account the specific needs of a component market. Based on these semantic concepts, we present a new specification language QML/CS that can be used to model non-functional product properties of components and component-based software systems. [ABSTRACT FROM AUTHOR]

Abstract: After studying how undoing of events of irreversibly aging processes complicates in the presence of urgent events or occasionally suspended subprocesses, we propose a reversibility operator for the standard process-algebraic specification language E-LOTOS, whose recently proposed true-concurrency semantics is based on enhanced event structures (EESs). With this operator, the reversibility of events executed by a real-time process and the urgency of their undoing can be specified with respect to their external appearance and the time elapsed since their execution. To facilitate definition of the operator, we introduce a very fine control of event undoing into the general EESs. [Copyright &y& Elsevier]

Maintaining integrity constraints in information systems is a real issue. In our previous work, we have defined a formal approach that derives B formal specifications from a UML description of the system. Basically, the generated B specification is composed of a set of variables modeling data and a set of operations representing transactions. The integrity constraints are directly specified as B invariant properties. So far, the operations we generate establish only a reduced class of constraints. In this paper, we describe a systematic approach to identify preconditions that take a larger class of invariants into account. The key idea is the definition of rewriting and simplification rules that we apply to the B invariants. [ABSTRACT FROM AUTHOR]

Abstract: This paper presents a general and formal approach to designing robot controllers. It is based on structuring the controller into subsystems dealing with effectors, receptors, inter-agent transmission and internal memory. The behaviour of the controller is governed by transition functions. They are the basis for the definitions of robot behaviours. A systematic method of partitioning the task of a robot into separate bio-inspired elementary behaviours and the method of composing those behaviours into actions performed by the robot in the real environment are presented. Those general considerations are illustrated by an example of the design of behavioural controllers for robots executing a joint transportation task. The robots only observe the effects of the others activities in the environment (stigmergy). The presented specific solution to the joint box pushing example has its own merits, however the paper focuses on the general aspects of formal approach to controller design of multi-robot systems. [Copyright &y& Elsevier]

The DatagramCongestion Control Protocol (DCCP) is a new transport protocol standardized by the Internet Engineering Task Force (IETF) in March 2006. This paper discusses the specification of the connectionmanagement and synchronization procedures of DCCP using Coloured Petri Nets (CPNs). After introducing the protocol, we describe how the CPN model evolved as DCCP was being developed. We focus on our experience of incremental enhancement in the hope that this will provide guidance to those attempting to build complex protocol models. In particular, we discuss how the architecture, data structures and specification style of the model evolved as DCCP was developed. We finally recommend a procedure-based style once the standard is stable. The impact of this work on the DCCP standard and our interaction with IETF is also briefly discussed. [ABSTRACT FROM AUTHOR]

The abstraction inherent in most specifications and the need to specify nondeterministic programs are two well-known sources of nondeterminism in formal specifications. In this paper, we present a Z-based formalism by which one can specify bounded, unbounded, erratic, angelic, demonic, loose, strict, singular, and plural nondeterminism. To interpret our specifications, we use a constructive set theory, called CZ set theory, instead of the classical set theory Z. We have chosen CZ since it allows us to investigate the notion of nondeterminism from the formal program development point of view. In this way, we formally construct functional programs from Z specifications and then probe the effects of the initially specified nondeterminism on final programs. Our investigation shows that without specifying nondeterminism explicitly, the effects of the nondeterminism involved in initial specifications will not be preserved in final programs. We prove that using the new formalism, proposed by this paper, for writing nondeterministic specifications leads to programs that preserve the initially specified modalities of nondeterminism. [ABSTRACT FROM AUTHOR]

Abstract: This paper provides formal specification of interactions in typical public health surveillance systems involving healthcare agencies at local, state and federal levels. Although few standards exist for exchange of healthcare information, there is a general lack of formal models of the protocols involved in the interactions between the agencies. The quality of medical care provided is an end result of a well designed choreography of diverse services provided by different healthcare entities. One of the major challenges in this field appears to be explicit formal specification of such interactions. Such formal specification work is the first step leading to both design and verification of important properties of public healthcare systems. -calculus is a formal modeling technique for precise specification of semantics in interacting concurrent systems where mobility is involved. Two different configurations of public health surveillance systems are modelled using -calculus in this paper. [Copyright &y& Elsevier]