Making sense of runtime architecture for mobile phone software
Making sense of runtime architecture for mobile phone software.
2,847 papers · page 130 of 143
Bogor: an extensible and highly-modular software model checking framework
Model checking is emerging as a popular technology for reasoning about behavioral properties of a wide variety of software artifacts including: requirements models, architectural descriptions, designs, implementations, and process models. The complexity of model checking is well-…
Validating UML models against architectural profiles
The Unified Modeling Language (UML) has become a widely adopted standard in the software industry. While UML has established itself in detailed software design, its usage as an architecture description language is still taking its shape. In particular, there is a growing need for…
Runtime safety analysis of multithreaded programs
Foundational and scalable techniques for runtime safety analysis of multithreaded programs are explored in this paper. A technique based on vector clocks to extract the causal dependency order on state updates from a running multithreaded program is presented, together with algor…
Consistency techniques for interprocedural test data generation
This paper presents a novel approach for automated test data generation of imperative programs containing integer, boolean and/or float variables. It extends our previous work to programs with procedure calls and arrays. A test program (with procedure calls) is represented by an …
Towards an engineering tool for implementing reusable distributed control systems
The IEC model for distributed control systems (DCSs) was adopted for the implementation of a new generation engineering tool. However, it was found that this approach does not exploit all the benefits of the object and component technologies. In this paper, we present the enhance…
Adapting side effects analysis for modular program model checking
There is a widely held belief that whole program analysis is intractable for large complex software systems, and there can be little doubt that this is true for program analyses based on model checking. Model checking selected program components that comprise a cohesive unit, how…
Behaviour model elaboration using partial labelled transition systems
State machine based formalisms such as labelled transition systems (LTS) are generally assumed to be complete descriptions of system behaviour at some level of abstraction: if a labelled transition system cannot exhibit a certain sequence of actions, it is assumed that the system…
Designing and implementing a family of intrusion detection systems
Intrusion detection systems are distributed applications that analyze the events in a networked system to identify malicious behavior. The analysis is performed using a number of attack models (or signatures) that are matched against a specific event stream. Intrusion detection s…
Reverse engineering framework reuse interfaces
Object-oriented application frameworks provide an established way of reusing the design and implementation of applications in a specific domain. Using a framework for creating applications is not a trivial task, however, and special tools are needed for supporting the process. To…
Verified systems by composition from verified components
This paper presents an approach to integration of model checking into component-based development of software systems. This approach assists in development of highly reliable component-based software systems and reduces the complexity of verifying these systems by utilizing their…
ARCHER: using symbolic, path-sensitive analysis to detect memory access errors
Memory corruption errors lead to non-deterministic, elusive crashes. This paper describes ARCHER (ARray CHeckER) a static, effective memory access checker. ARCHER uses path-sensitive, interprocedural symbolic analysis to bound the values of both variables and memory sizes. It eva…
Protecting C programs from attacks via invalid pointer dereferences
Writes via unchecked pointer dereferences rank high among vulnerabilities most often exploited by malicious code. The most common attacks use an unchecked string copy to cause a buffer overrun, thereby overwriting the return address in the function's activation record. Then, when…
Searching for points-to analysis
The complexity of points-to analysis is well understood, but the approximations used to carry out points-to analysis efficiently are less well understood. In this paper we characterize points-to analysis as a reachability problem on a program's state space. Reachability analysis …
A micro-economic approach to conflict resolution in mobile computing
Mobile devices, such as mobile phones and personal digital assistants, have gained wide-spread popularity. These devices will increasingly be networked, thus enabling the construction of distributed mobile applications. These have to adapt to changes in context, such as variation…
Supporting aggregation in fine grained software configuration management
Fine-grained software configuration management offers substantial benefits for large-scale collaborative software development, enabling a variety of interesting and useful features including complexity management, support for aspect-oriented software development, and support for …
Containment units: a hierarchically composable architecture for adaptive systems
Software is increasingly expected to run in a variety of environments. The environments themselves are often dynamically changing when using mobile computers or embedded systems, for example. Network bandwidth, available power, or other physical conditions may change, necessitati…
Model exploration with temporal logic query checking
A temporal logic query is a temporal logic formula with placeholders. Given a model, a solution to a query is a set of assignments of propositional formulas to placeholders, such that replacing the placeholders with any of these assignments results in a temporal logic formula tha…
The logic of bugs
Real-life bugs are successful because of their unfailing ability to adapt. In particular this applies to their ability to adapt to strategies that are meant to eradicate them as a species. Software bugs have some of these same traits. We will discuss these traits, and consider wh…
Egocentric context-aware programming in ad hoc mobile environments
Some of the most dynamic systems being built today consist of physically mobile hosts and logically mobile agents. Such systems exhibit frequent configuration changes and a great deal of resource variability. Applications executing under these circumstances need to react continuo…