3,458 papers · page 145 of 173
This paper describes a framework that allows for reasoning about and verification of concurrent statecharts with real-time constraints subject to semantic variations. The major problems addressed by this paper include the capture of multiple semantic variations of real-time state…
To realize the benefits of Aspect Oriented Programming (AOP), developers must refactor active and legacy code bases into an AOP language. When refactoring, developers first need to identify refactoring candidates, a process called aspect mining. Humans perform mining by using a v…
Automated consistency checking of UML models becomes necessary as models grow in size and complexity. Because the UML metamodel does not enforce model consistency, there are no guidelines as how to approach the consistency problem. Current solutions are partial and tools are most…
User-session-based testing of web applications gathers user sessions to create and continually update test suites based on real user input in the field. To support this approach during maintenance and beta testing phases, we have built an automated framework for testing web-based…
Virtual humans are computer generated characters that can populate games or simulations. The behaviors of virtual humans are not scripted, but instead they use sophisticated AI techniques to reason about their environment and events as they unfold. Based on that reasoning, the vi…
Distributed applications typically interact with a number of heterogeneous and autonomous components that evolve independently. Methodical development of such applications can benefit from approaches based on domain-specific languages (DSLs). However, the evolution and customizat…
We propose a model-based framework for developing self-monitoring embedded programs with temporal logic specifications. In our framework the requirement specification of an embedded program is encoded in the temporal logic MEDL. We propose an algorithm that synthesizes a model-ba…
During software maintenance, some non-functional properties may be lost. This is due to the lack of an explicit definition of their links with the corresponding architectural choices. In this paper, we present a solution that automates the checking of non-functional properties af…
We present a parameterized interpreter for modeling aspect-oriented mechanisms. The interpreter takes several parameters to cover different AOP mechanisms found in AspectJ, Hyper/J, and Demeter. The interpreter helps our understanding of the AOP mechanisms in two ways. First, its…
We present a new model checking algorithm for verifying computation tree logic (CTL) properties. To our knowledge, this is the first CTL model checking algorithm for infinite state systems that can also handle fairness constraints. Our technique is based on using language inferen…
We consider the problem of test input generation for code that manipulates complex data structures. Test inputs are sequences of method calls from the data structure interface. We describe test input generation techniques that rely on state matching to avoid generation of redunda…
Localizing the cause(s) of an observable error lies at the heart of program debugging. Fault localization often proceeds by comparing the failing program run with some "successful" run (a run which does not demonstrate the error). An issue here is to generate or choose a "suitabl…
Engineering distributed systems is a challenging activity. This is partly due to the intrinsic complexity of distributed systems, and partly due to the practical obstacles that developers face when evaluating and tuning their design and implementation decisions.This paper address…
Current formal software engineering methodologies provide a vast array of languages for specifying correctness properties, as well as a wide assortment automated tools that aid in the verification of specified properties. Unfortunately, the implementation of each such tool requir…
Domain-specific languages (DSLs) assist a domain expert (or end-user) in writing a software program using idioms that are closer to the abstractions found in a specific problem domain. Language tool support for DSLs is lacking, however, when compared to the capabilities provided …
In test generation based on model-checking, white-box test criteria are represented as trap conditions written in a temporal logic. A model checker is used to refute trap conditions with counter-examples. From a feasible counter-example test inputs are then generated. The major p…
This paper presents UMLDiff, an algorithm for automatically detecting structural changes between the designs of subsequent versions of object-oriented software. It takes as input two class models of a Java software system, reverse engineered from two corresponding code versions. …
This paper presents a formal approach to threat-driven modeling and verification of secure software using aspect-oriented Petri nets. Based on the behavior model of intended functions, we identify and build formal models of security threats, which are potential misuses and anomal…
This paper develops a framework for solving temporal-logic query-checking problems for a class of infinite-state system models that compute with integer-valued variables (so-called Presburger systems, in which Presburger formulas are used to define system behavior). The temporal-…
Article Share on In regression testing selection when source code is not available Author: Jiang Zheng North Carolina State University, Raleigh, NC North Carolina State University, Raleigh, NCView Profile Authors Info & Claims ASE '05: Proceedings of the 20th IEEE/ACM Internation…