3,458 papers · page 142 of 173
Concurrent programs are notorious for containing errors that are difficult to reproduce and diagnose. Two common kinds of concurrency errors are data races and atomicity violations (informally, atomicity means that executing methods concurrently is equivalent to executing them se…
We present an experimental study which demonstrates that model checking techniques can be effective in finding synchronization errors in safety critical software when they are combined with a design for verification approach. We apply the concurrency controller design pattern to …
The purpose of the workshop is to convene researchers, developers, and government and industrial users of software security assurance (SSA) tools to refine the taxonomy of flaws and the taxonomy of SSA tool functions, converge on which SSA functions should first have specificatio…
Design patterns are widely used by designers and developers for building complex systems in object-oriented programming languages such as Java. However, systems evolve over time, increasing the chance that the pattern in its original form will be broken.To verify that a design pa…
Combinatorial approaches to testing are used in several fields, and have recently gained momentum in the field of software testing through software interaction testing. One-test-at-a-time greedy algorithms are used to automatically construct such test suites. This paper discusses…
The structure of the coupling relation on design decisions is a key factor influencing the evolvability properties and the economic value of a design. The work of Baldwin and Clark is an important step toward a theory of the relationship between structure and value. A key step to…
In earlier work we have argued that formal process definitions can be useful in improving our understanding and performance of software development processes. There has, however, been considerable sentiment that formalized processes cannot capture the creative process of software…
Quasi-random sequences, also known as low-discrepancy or low-dispersion sequences, are sequences of points in an n-dimensional unit hypercube. These sequences have the property that points are spread more evenly throughout the cube than random point sequences, which result in reg…
Automated testing typically uses specifications to drive the generation of test inputs and/or the checking of program outputs. Many software systems have structurally complex inputs that cannot be adequately described using simple formalisms such as context-free grammars. In orde…
We present a uniform verification method of safety properties for classes of parameterized protocols. Properties like mutual exclusion or cache coherence are automatically verified for any number of similar processes communicating by broadcast and rendezvous. The protocols are sp…
The current trend in debugging and testing is to cross-check information collected during several executions. Jones et al., for example, propose to use the instruction coverage of passing and failing runs in order to visualize suspicious statements. This seems promising but lacks…
The goal of this workshop is to explore new technologies, underlying principles, and general methodologies for supporting software certificate management. Software certification demonstrates the reliability, safety, or security of software systems in such a way that it can be che…
Component technologies are increasingly being used for building enterprise systems, as they can address complex functionality and flexibility problems and reduce development and maintenance costs. Nonetheless, current component technologies provide little support for predicting a…
The Nix software deployment system is based on the paradigm of transparent source/binary deployment: distributors deploy descriptors that build components from source, while client machines can transparently optimise such source builds by downloading pre-built binaries from remot…
Many distributed systems using IP-based communication protocols consist of chains of components that run concurrently and communicate asynchronously with their neighbours through ports. We present a compositional reasoning method using model checking and theorem proving to verify…
Major software development standards mandate the establishment of trace links among software artifacts such as requirements, architectural elements, or source code without explicitly stating the required level of detail of these links. However, the level of detail vastly affects …
Visual Languages (VLs) play an important role in software system development. Especially when looking at well-defined domains, a broad variety of domain specific visual languages are used for the development of new applications. These languages are typically developed specificall…
Spreadsheets are widely used in all kinds of business applications. Numerous studies have shown that they contain many errors that sometimes have dramatic impacts. One reason for this situation is the low-level, cell-oriented development process of spreadsheets.We improve this pr…
The PLUSS approach (Product Line Use case modeling for Systems and Software engineering) is a domain modeling method tailored towards the development of long lived software intensive systems. PLUSS provides means to maintain a common and complete use case model for a whole family…