2,847 papers · page 128 of 143
One of the benefits of finite-state verification (FSV) tools, such as model checkers, is that a counterexample is provided when the property cannot be verified. Not all counterexamples, however, are equally useful to the analysts trying to understand and localize the fault. Often…
Constructing comprehensive operational models of intended system behaviour is a complex and costly task. Consequently, practitioners have adopted techniques that support incremental elaboration of partial behaviour descriptions. A noteworthy example is the wide adoption of scenar…
Constructing rigorous models for analysing the behaviour of concurrent and distributed systems is a complex task. Our aim is to facilitate model construction. Scenarios provide simple, intuitive, example based descriptions of the behaviour of component instances in the context of…
This paper introduces declarative event patterns (DEPs) as a means to implement protocols while improving their traceability, comprehensibility, and maintainability. DEPs are descriptions of sequences of events in the execution of a system that include the ability to recognize pr…
These days, if you say that you are doing research in the area of computer security you instantly receive attention. Sadly, the same cannot be said of software engineering. But are the two areas really so different? Both seem to be concerned with issues that range from the finely…
Memory-related errors, such as buffer overflows and dangling pointers, remain one of the principal reasons for failures of C programs. As a result, a number of recent research efforts have focused on the problem of dynamic detection of memory errors in C programs. However, existi…
We address the problem of refining and completing a partially specified high-level design model and a partially-defined mapping from source code to design model. This is related but not identical to tasks that have been automated with a variety of reverse engineering tools to sup…
Five modern static analysis tools (ARCHER, BOON, Poly-Space C Verifier, Splint, and UNO) were evaluated using source code examples containing 14 exploitable buffer overflow vulnerabilities found in various versions of Sendmail, BIND, and WU-FTPD. Each code example included a "BAD…
Quantitative performance analysis of software systems should be integrated in the software development process from the early stages. Software performance modelling and analysis allows the software designer to address performance related issues such as the comparison of design al…
Most applications developed today rely on a given middleware platform which governs the interaction between components, the access to resources, etc. To decide, which platform is suitable for a given application (or more generally, to understand the interaction between applicatio…
Step-wise refinement (SWR) asserts that complex programs can be derived from simple programs by progressively adding features. The length of a program specification is the number of features that the program has. Critical to the scalability of SWR are multi-dimensional models tha…
This paper presents PLUTO, a simple and intuitive methodology to manage the testing process of product lines, described as Product Lines Use Cases (PLUCs). PLUCs are an extension of the well-known Cockburn's Use Cases, a notation based on natural language descriptions of requirem…
Model checking and other finite-state analysis techniques have been very successful when used with hardware systems and less successful with software systems. It is especially difficult to analyze software systems developed with the implicit invocation architectural style because…
Real-time, reactive, and embedded systems are widely used throughout society (e.g., flight control, railway signaling, vehicle management, medical devices, and many others). For real-time, interrupt-driven software, timely interrupt handling is part of correctness. It is vital fo…
Statistical Process Control (SPC) is a powerful tool to control the quality of processes. It assists management personnel in the identification of problems and actions to be taken to bring a process into a stable state. SPC has been applied in various fields, including the Softwa…
Automated finite-state verification techniques have matured considerably in the past several years, but state-space explosion remains an obstacle to their use. Theoretical lower bounds on complexity imply that all of the techniques that have been developed to avoid or mitigate st…
Existing software engineering and organization development literature acknowledges that there are fundamental operational differences between small and large organizations. Despite this recognition, there has been no attempt to verify whether small and large software organization…
ebXML is becoming the new international standard for the specification and deployment of complex B2B transactions over the internet. ebXML transactions are inherently distributed, involving many actors exchanging XML messages with each other according to complex flows and rules. …
Model checking is an automated technique for verifying that a system satisfies a set of required properties. Such properties are typically expressed as temporal logic formulas, in which atomic propositions are predicates over state variables of the system. In event-based system d…
Current techniques for the verification of software as e.g. model checking are limited when it comes to the verification of complex distributed embedded real-time systems. Our approach addresses this problem and in particular the state explosion problem for the software controlli…