3,458 papers · page 155 of 173
The Unified Modeling Language (UML) supports a wide range of diagrams for modeling software development concerns. UML diagrams are independent but connected; their meta-model describes them under a common roof. Despite the advances of UML, we found that the problem of ensuring co…
It is becoming increasingly desirable to incorporate commercial-off-the-shelf (COTS) tools as software components into larger software systems. Due to their large user base, COTS tools tend to be cheap, reasonably reliable, and functionally powerful. Reusing them as components ha…
We propose to view programs as abstract data types and to perform program changes by applying well-defined operations on programs. The ADT view of programs goes beyond the approach of syntax-directed editors and proof-editors since it is possible to combine basic update operation…
In order to understand, analyze and modify software, we commonly examine and manipulate its architecture. For example, we may want to examine the architecture at different levels of abstraction. We can view such manipulations as architectural transformations, and more specificall…
Formalizing security requirements has received a significant attention since the 70s. However a general method for specifying security requirements is still missing. Especially, little work has been presented on specifying and verifying that a given application is a secure resour…
Erlang is a functional programming language with support for concurrency and message passing communication that is used at Ericsson for developing telecommunication applications. We consider the challenge of verifying temporal properties of systems programmed in Erlang with dynam…
The Spin model checker is a system that has been used to model and analyze a large number of applications in several domains including the aerospace industry. One of the novelties of Spin is its relatively simple specification language, Promela, as well as the powerful abilities …
We argue that the evolution of requirements specifications can be supported by a cycle composed of two phases: analysis and revision. We investigate an instance of such a cycle, which combines two techniques of logical abduction and inductive learning to analyze and revise specif…
This paper presents an approach to checking a running program against Linear Temporal Logic (LTL) specifications. LTL is a widely used logic for expressing properties of programs viewed as sets of executions. Our approach consists of translating LTL formulae to finite-state autom…
We propose a novel way of automating statistical structural testing of software, based on the combination of uniform generation of combinatorial structures, and of randomized constraint solving techniques. More precisely, we show how to draw test cases which balance the coverage …
The construction of interactive server-side Web applications differs substantially from the construction of traditional interactive programs. In contrast, existing Web programming paradigms force programmers to save and restore control state between user interactions. We present …
Concurrent Class Machines are a novel state-machine model that directly captures a variety of object-oriented concepts, including classes and inheritance, objects and object creation, methods, method invocation and exceptions, multithreading and abstract collection types. The mod…
Most distributed system specifications have performance benchmark requirements. However, determining the likely performance of complex distributed system architectures during development is very challenging. We describe a system where software architects sketch an outline of thei…
Electronic data interchange (EDI) systems are used in many domains to support inter-organisational information exchange. To get systems using different EDI message formats to communicate, complex message translations (where data must be transformed from one EDI message format int…
Module cohesion describes the degree to which different actions performed by a module contribute towards a unified function. High module cohesion is a desirable property of a program. The program modifications during successive maintenance interventions can have negative effect o…
A high-bandwidth, always-on Internet connection makes computers in homes and small offices attractive targets for network-based attacks. Network security gateways can protect such vulnerable hosts from attackers, but differing sets of customer needs require different feature mixe…
The inspection of early life-cycle artifacts such as requirement documents promises great benefits. However, research demonstrates that the inspection process is complex and expensive and that tool support would be highly desirable. Existing inspection tools focus largely on the …
We present a rewriting algorithm for efficiently testing future time Linear Temporal Logic (LTL) formulae on finite execution traces. The standard models of LTL are infinite traces, reflecting the behavior of reactive and concurrent systems which conceptually may be continuously …
Although formal methods have been successfully applied in various industrial applications, their use in software development is still restricted to individual case studies. To overcome this situation we aim at a methodology for an evolutionary formal software development which al…
In recent years the necessity for handling different aspects of the system separately has introduced the need to represent SA (software architectures) from different viewpoints. In particular, behavioral views are recognized to be one of the most attractive features in the SA des…