Article Patterns in property specifications for finite-state verification Share on Authors: Matthew B. Dwyer Kansas State University, Department of Computing and Information Sciences, Manhattan, KS KSView Profile , George S. Avrunin University Massachusetts, Mathematics Statistics, Amherst, MA MAView James C. Corbett Hawai'i, Computer Science, Honolulu, HI HIView Authors Info & Claims ICSE '99: Proceedings the 21st international conference Software engineeringMay 1999 Pages...

Finite-state verification techniques, such as model checking, have shown promise a cost-effective means for finding defects in hardware designs. To date, the application of these techniques to software has been hindered by several obstacles. Chief among is problem constructing finite-state that approximates executable behavior system interest. Current best-practice involves hand-construction models which expensive (prohibitive all but smallest systems), prone errors (which can result...

Article Free Access Share on Property specification patterns for finite-state verification Authors: Matthew B. Dwyer Kansas State University, Department of Computing and Information Sciences, 234 Nichols Hall Manhattan, KS KSView Profile , George S. Avrunin University Massachusetts, Mathematics Statistics, Box 34515, Amherst, MA MAView James C. Corbett Hawai'i, Computer Science, Honolulu, HI HIView Authors Info & Claims FMSP '98: Proceedings the second workshop Formal methods in software...

Researchers have explored the application of combinatorial interaction testing (CIT) methods to construct samples drive systematic software system configurations. Applying CIT highly-configurable systems is complicated by fact that, in many such systems, there are constraints between specific configuration parameters that render certain combinations invalid. Many algorithms lack a mechanism avoid these. In recent work, automated constraint solving been combined with search-based construction...

Detecting and characterizing the effects of software changes is a fundamental component maintenance. Version differencing information can be used to perform version merging, infer change characteristics, produce program documentation, guide re-validation. Existing techniques for code changes, however, are imprecise leading unnecessary maintenance efforts.

Combinatorial interaction testing (CIT) is a method to sample configurations of software system systematically for testing. Many algorithms have been developed that create CIT samples, however few considered the practical concerns arise when adding constraints between combinations options. In this paper, we survey constraint handling techniques in existing and discuss challenges they present. We examine two highly-configurable systems quantify nature real systems. then present general...

Model checking is emerging as a popular technology for reasoning about behavioral properties of wide variety software artifacts including: requirements models, architectural descriptions, designs, implementations, and process models. The complexity model well-known, yet cost-effective analyses have been achieved by exploiting, example, naturally occurring abstractions semantic target artifact. artifacts. Adapting tool to exploit this kind domain knowledge often requires in-depth the tool's...

In this paper we present an approach, based on data flow analysis, that can provide cost-effective analysis of concurrent programs with respect to explicitly stated correctness properties. Using a developer specifies property program as pattern selected events and asks the verify all or no executions satisfy given property. We have developed family polynomial-time, conservative anlysis algorithms support reasoning about these questions. To overcome traditional inaccuracies static also range...

The analysis of constraints plays an important role in many aspects software engineering, for example constraint satisfiability checking is central to symbolic execution. However, the norm recompute results each analysis. We propose a different approach where every call solver wrapped check see if result not already available. While tools use some form caching, novelty our persistence across runs, programs being analyzed, analyses and even physical location. Achieving such reuse requires...

The continued development of efficient automated decision procedures has spurred the resurgence research on symbolic execution over past decade. Researchers have applied to a wide range software analysis problems including: checking programs against contract specifications, inferring bounds worst-case performance, and generating path-adequate test suites for widely used library code.

The use of component models such as Enterprise Java Beans and the CORBA Component Model (CCM) in application development is expanding rapidly. Even real-time safety/mission-critical domains, component-based beginning to take hold a mechanism for incorporating non-functional aspects real-time, quality-of-service, distribution. To form an effective basis systems, we believe that support reasoning about correctness properties designs essential.In this paper, present Cadena -- integrated...

Software product line modeling has received a great deal of attention for its potential in fostering reuse software artifacts across development phases. Research on the testing phase, focused identifying test cases instances. While this offers reductions effort given instance, it does not focus and leverage fundamental abstraction that is inherent lines - variability.In paper, we illustrate how rich notations can be mapped onto an underlying relational model captures variability feasible...

The notion of control dependence underlies many program analysis and transformation techniques. Despite being widely used, existing definitions approaches to calculating are difficult apply directly modern structures because these make substantial use exception processing increasingly support reactive systems designed run indefinitely. This article revisits foundational issues surrounding dependence, develops algorithms for computing several variations that can be applied structures. To...

Combinatorial interaction testing (CIT) is a cost-effective sampling technique for discovering faults in highly configurable systems. Recent work with greedy CIT algorithms efficiently supports constraints on the features that can coexist configuration. But when single system configuration expensive, techniques perform worse than meta-heuristic because they produce larger samples. Unfortunately, current are inefficient present. We investigate sources of inefficiency, focusing simulated...

Load tests aim to validate whether system performance is acceptable under peak conditions. Existing test generation techniques induce load by increasing the size or rate of input. Ignoring particular input values, however, may lead suites that grossly mischaracterize a system's performance. To address this limitation we introduce mixed symbolic execution based approach unique in how it 1) favors program paths associated with measure interest, 2) operates an iterative-deepening beam-search...

There are many ways to express parallel programs: message-passing libraries (MPI) and multithreading/GPU language extensions such as OpenMP, Pthreads, CUDA, but a few. This multitude creates serious challenge for developers of software verification tools: it takes enormous effort develop tools, each development typically targets one small part the concurrency landscape, with little sharing techniques code among efforts.

Numerous researchers have reported success in reasoning about properties of small programs using finite-state verification techniques. We believe, as do most this area, that order to scale those initial successes realistic programs, aggressive abstraction program data will be necessary. Furthermore, we believe make abstraction-based usable by non-experts significant tool support required.In paper, describe how several different analysis and transformation techniques are integrated into the...

Finite-state verification techniques, such as model checking, have shown promise a cost-effective means for finding defects in hardware designs. To date, the application of these techniques to software has been hindered by several obstacles. Chief among is problem constructing finite-state that approximates executable behavior system interest. Current best-practice involves hand-construction models which expensive (prohibitive all but smallest systems), prone errors (which can result...

This article describes FLAVERS, a finite-state verification approach that analyzes whether concurrent systems satisfy user-defined, behavioral properties. FLAVERS automatically creates compact, event-based model of the system supports efficient dataflow analysis. achieves this efficiency at cost precision. Analysts, however, can improve precision analysis results by selectively and judiciously incorporating additional semantic information into an analysis.We report on empirical study...

A key problem in model checking open systems is environment modeling (i.e., representing the behavior of execution context system under analysis). Software are fundamentally since their dependent on patterns invocation components and values defined outside but referenced within system. Whether reasoning about whole programs or program components, an abstract can be essential enabling sufficiently precise yet tractable verification. In this paper, we describe approach to generating...

Unit test cases are focused and efficient. System tests effective at exercising complex usage patterns. Differential unit (DUT) a hybrid of system tests. They generated by carving the components, while executing case, that influence behavior target unit, then re-assembling those components so can be exercised as it was test. We conjecture DUTs retain some advantages tests, automatically inexpensively generated, have potential for revealing faults related to intricate executions. In this...