2,847 papers · page 131 of 143
Goal orientation is an increasingly recognized paradigm for eliciting, modeling, specifying and analyzing software requirements. Goals are statements of intent organized in AND/OR refinement structures; they range from high-level, strategic concerns to low-level, technical requir…
Feature-oriented software designs capture many interesting notions of cross-cutting, and offer a powerful method for building product-line architectures. Each cross-cutting feature is an independent module that fundamentally yields an open system from a verification perspective. …
In this paper, we address the integration of a distribution dimension in an architectural approach to system development and evolution based on the separation between coordination and computation. This third dimension allows us to separate key concerns raised by mobility, thus co…
Program slicing is a potentially useful analysis for aiding program understanding. However, slices of even small programs are often too large to be generally useful. Imprecise pointer analyses have been suggested as one cause of this problem. In this paper, we use dynamic points-…
Static checking can verify the absence of errors in a program, but often requires written annotations or specifications. As a result, static checking can be difficult to use effectively: it can be difficult to determine a specification and tedious to annotate programs. Automated …
We propose a unifying framework for model-based specification notations. Our framework captures the execution semantics that are common among model-based notations, and leaves the distinct elements to be defined by a set of parameters. The basic components of a specification are …
We propose an extension to Message Sequence Charts called Triggered Message Sequence Charts (TMSCs) that are intended to capture system specifications involving nondeterminism in the form of conditional scenarios. The visual syntax of TMSCs closely resembles that of MSCs; the sem…
Scenario-based specifications such as Message Sequence Charts (MSCs) are popular for requirement elicitation and specification. MSCs describe two distinct aspects of a system: on the one hand they provide examples of intended system behaviour and on the other they outline the sys…
Security is a very important issue in information processing, especially in open network environments like the Internet. The Common Criteria (CC)is the standard requirements catalogue for the evaluation of security critical systems. Using the CC, a large number of security requir…
This paper explores the idea that redundant operations, like type errors, commonly flag correctness errors. We experimentally test this idea by writing and applying four redundancy checkers to the Linux operating system, finding many errors. We then use these errors to demonstrat…
Consider the execution of a failing program as a sequence of program states. Each state induces the following state, up to the failure. Which variables and values of a program state are relevant for the failure? We show how the Delta Debugging algorithm isolates the relevant vari…
The limitations of client/server systems become evident in an Internet-scale distributed environment. P2P systems offer an alternative to traditional client/server systems: Every node acts both as a client and a server and "pays" its participation by providing access to its compu…
Conventional type systems specify interfaces in terms of values and domains. We present a light-weight formalism that captures the temporal aspects of software component interfaces. Specifically, we use an automata-based language to capture both input assumptions about the order …
In this paper we report on the 8th European Workshop on Software Process Technology held in Witten (Germany) in June 2001. We also report on the outcome of a working session about the future directions of research in software process technology that will be addressed in the next …
We use the formal language Z to specify and analyze the security service of CORBA. In doing so, we tackle the problem of how one can apply lightweight formal methods to improve the precision and aid the analysis of a substantial, informal specification. Our approach is scenario-d…
Although software components have become one of the mainstream technologies, they still lack a supportive versioning scheme. This paper describes a system for revision identification of released components with well defined semantics. It is based on the analysis of changes in the…
Model checking techniques have not been effective in important classes of software systems characterized by large (or infinite) input domains with interrelated linear and non-linear constraints over the input variables. Various model abstraction techniques have been proposed to a…
We report on a tool we have developed that automates the derivation of tests from specifications. The tool implements conformance testing techniques to derive symbolic tests that incorporate their own oracles from formal operational specifications. It was applied for testing a si…
Layered architecture in operating system code is often compromised by execution path-specific customizations such as prefetching, page replacement and scheduling strategies. Pathspecific customizations are difficult to modularize in a layered architecture because they involve dyn…
Safety critical systems require to be highly reliable and thus special care is taken when verifying them in order to increase the confidence in their behavior. This paper addresses the problem of formal verification of safety critical systems by providing empirical evidence of th…