ISSTA

Requirements of event-based systems can be automatically analyzed to determine if certain safety properties hold. However, we lack comparable methods to verify that implementations maintain the properties guaranteed by the requirements. We have built a ...

This paper introduces Aslantest, a symbolic execution tool for the formal specification language Aslan. Aslan is a state-based specification language built on first-order predicate calculus with equality. Aslantest animates Aslan specifications and ...

Books on software engineering methodologies talk about the significance and need for designing consistent and complete specifications during the requirement analysis and design stages of a software development cycle. There is, however, little (or at ...

A fundamental assumption of software testing is that there is some mechanism, an oracle, that will determine whether or not the results of a test execution are correct. In practice this is often done by comparing the output, either automatically or ...

A dynamic program slice is an executable part of the program whose behavior is identical, for the same program input, to that of the original program with respect to a variable(s) of interest at some execution position. It has been shown that dynamic ...

For certain structural testing criteria a significant proportion of tests instances are infeasible in the sense the semantics of the program implies that test data cannot be constructed that meet the test requirement. This paper describes the design and ...

Communication protocols are the rules that govern the communication between the different components within a distributed computer system. Since protocols are implemented in software and/or hardware, the question arises whether the existing hardware and ...

A timeline is a linear, graphical visualization of events over time. For example, in concurrent application, events would represent state changes for some system object (such as a task or variable). A timeline display generator creates the graphical ...

Few would question that software testing is a necessary activity for assuring software quality, yet the typical testing process is a human intensive activity and as such, it is unproductive, error-prone, and often inadequately done. Moreover, testing is ...

In previously reported research we designed and analyzed algorithms that improved upon the run time complexity of all known weak and strong mutation analysis methods at the expense of increased space complexity. Here we describe a new serial strong ...

Non-determinism makes testing concurrent software difficult. We consider how pre-run-time state-space analysis can be used to aid in testing implementations of concurrent software. State-space analysis techniques have the advantage in principle of ...

Static analysis of Ada tasking programs has been hindered by the well known state explosion problem that arises in the verification of concurrent systems. Many different techniques have been proposed to combat this state explosion. All proposed methods ...

We present a first report on our PARTS toolset for the automated static analysis of real-time systems. The PARTS toolset is based upon a timed extension of Petri nets.

Our simple time Petri nets or STP nets are specifically aimed at facilitating real-...