Abstract Maintaining software is cumbersome when method argument constraints are undocumented. To reveal them, previous work learned preconditions from exemplary valid and invalid method arguments. In practice, it would be highly beneficial to know class invariants, too, because functionality added during software maintenance must not break them. Even more so than method preconditions, class invariants are rarely documented and often cannot completely be inferred automatically, especially for objects exhibiting complex state such as dynamic data structures. This paper presents a novel dynamic approach to learning class invariants, thereby complementing related work on learning method preconditions. We automatically synthesize assertions from an adjustable assertion grammar to distinguish valid and invalid objects. While random walks generate valid objects, a combination of bounded-exhaustive testing techniques and behavioral oracles yield invalid objects. The utility of our approach for code comprehension and software maintenance is demonstrated by comparing our learned invariants to documented invariant validation methods found in real-world Java classes and to the invariants detected by the Daikon tool.

Understanding complex software components is crucial for software evolution and maintenance. While documentation on software behavior is often available and sufficient for software reusability, maintenance requires additional information such as internal state constraints. While, these constraints, typically encoded as class invariants in object-oriented programming, are rarely documented, dynamic class invariant learning approaches can be used to extract candidate invariants from concrete object states. Recent approaches leverage negative training data to assess invariant completeness; however, a diverse set of invalid object states is particularly challenging to obtain. This paper proposes a novel approach for the automatic creation of invalid objects by combining program mutation with object state space exploration, thereby reaching invalid objects that cannot be constructed using the original class definition. Evaluating our approach on data structures, including those from the java.util package, revealed that it achieves a high object state space coverage. This demonstrates its potential for generating a diverse set of invalid objects suitable for class invariant learning.

Analyzing heap dumps containing complex dynamic data structures is essential when debugging modern software systems. However, existing tools for visualizing memory graphs can neither deal with corrupt structures such as binary trees exhibiting cycles, nor do they offer adequate abstractions when being confronted with large heaps. This paper presents MGE (Memory Graph Explorer), a memory analyzer and visualizer that combines a novel memory graph abstraction with an interactive visualization. MGE borrows ideas from separation logic and shape analysis to reveal relationships between memory nodes, name recognized structures such as doubly-linked lists and binary trees, and summarize complex structures. This summarization works for corrupt data structures, too, and is particularly powerful for large, nested structures due to its support for interactive (un)folding. MGE's utility for aiding program comprehension is illustrated by real-world and textbook examples and contrasted with existing debuggers.

Visualizing large memory graphs containing dynamic data structures and nested payload data is crucial when debugging legacy and modern software. However, existing visualization tools primarily focus on aggregating data structures and either rely on hard-coded patterns, generic heuristics, or predicates written in expressive logics. We present a novel heap pattern language for concisely and intuitively describing structural aspects of dynamic data structures and nested payload data. Evaluating a heap pattern on a memory graph yields a set of matching groups of interconnected objects, and analyzing these groups enables the construction of a multi-level hierarchy for memory graph visualization, where groups can individually be (un)folded to the desired level of detail. We have prototypically implemented our heap pattern language in the Memory Graph Explorer tool and illustrate its use for visualizing large memory graphs on real-world and textbook examples. Unlike existing tools, developers can now control the construction of hierarchies using heap patterns to flexibly and locally adjust the level of memory graph abstraction in an interactive graph visualization to highlight the areas demanding attention during debugging.

Abstract Interface theories based on Interface Automata (IA) are formalisms for the component-based specification of concurrent systems. Extensions of their basic synchronization mechanism permit the modelling of data, but are studied in more complex settings involving modal transition systems or do not abstract from internal computation. In this article, we show how de Alfaro and Henzinger’s original IA theory can be conservatively extended by shared memory data, without sacrificing simplicity or imposing restrictions. Our extension IA for shared Memory (IAM) decorates transitions with pre- and post-conditions over algebraic expressions on shared variables, which are taken into account by IA’s notion of component compatibility. Simplicity is preserved as IAM can be embedded into IA and, thus, accurately lifts IA’s compatibility concept to shared memory. We also provide a ground semantics for IAM that demonstrates that our abstract handling of data within IA’s open systems view is faithful to the standard treatment of data in closed systems.

This paper presents a novel algorithm for automatically learning recursive shape pred- icates from memory graphs, so as to formally describe the pointer-based data structures contained in a program. These predicates are expressed in separation logic and can be used, e.g., to construct efficient secure wrappers that validate the shape of data structures exchanged between trust boundaries at runtime. Our approach first decomposes memory graph(s) into sub-graphs, each of which exhibits a single data structure, and generates candidate shape predicates of increasing complexity, which are expressed as rule sets in Prolog. Under separation logic semantics, a meta-interpreter then performs a systematic search for a subset of rules that form a shape predicate that non-trivially and concisely captures the data structure. Our algorithm is implemented in the prototype tool ShaPE and evaluated on examples from the real-world and the literature. It is shown that our approach indeed learns concise predicates for many standard data structures and their implementation variations, and thus alleviates software engineers from what has been a time-consuming manual task.

Abstract Over the past two decades, de Alfaro and Henzinger’s interface automata (IA) have become a popular formal framework for the component-based specification of concurrent systems. IA’s parallel composition assumes that a component may wait on inputs but never on outputs, implying that an output must be consumed immediately or a communication error occurs. By now, the literature contains a number of semantics for IA: linear-time semantics based on traces observing communication errors , quiescence and/or divergence , as well as branching-time semantics based on alternating simulation . This article surveys these semantics from Rob van Glabbeek’s linear-time branching-time perspective, which does not consider settings with communication errors. We shed light onto the subtleties implied by IA’s pruning of all behaviour that might lead a component to autonomously enter an error state, and investigate when exactly de Alfaro and Henzinger’s restriction of input-determinism is needed. In addition, we introduce several new semantics for IA, in particular the linear-time ready semantics and the branching-time ready simulation .

Reverse engineering binary code is notoriously difficult and, especially, understanding a binary's dynamic data structures. Existing data structure analyzers are limited wrt. program comprehension: they do not detect complex structures such as skip lists, or lists running through nodes of different types such as in the Linux kernel's cyclic doubly-linked list. They also do not reveal complex parent-child relationships between structures. The tool DSI remedies these shortcomings but requires source code, where type information on heap nodes is available. We present DSIbin, a combination of DSI and the type excavator Howard for the inspection of C/C++ binaries. While a naive combination already improves upon related work, its precision is limited because Howard's inferred types are often too coarse. To address this we auto-generate candidates of refined types based on speculative nested-struct detection and type merging; the plausibility of these hypotheses is then validated by DSI. We demonstrate via benchmarking that DSIbin detects data structures with high precision.

As the complexity of malware grows, so does the necessity of employing program structuring mechanisms during development. While control flow structuring is often obfuscated, the dynamic data structures employed by the program are typically untouched. We report on work in progress that exploits this weakness to identify dynamic data structures present in malware samples for the purposes of aiding reverse engineering and constructing malware signatures, which may be employed for malware classification. Using a prototype implementation, which combines the type recovery tool Howard and the identification tool Data Structure Investigator (DSI), we analyze data structures in Carberp and AgoBot malware. Identifying their data structures illustrates a challenging problem. To tackle this, we propose a new type recovery for binaries based on machine learning, which uses Howard's types to guide the search and DSI's memory abstraction for hypothesis evaluation.

Comprehension of C programs containing pointer-based dynamic data structures can be a challenging task. To tackle this challenge we present Data Structure Investigator (DSI), a new dynamic analysis for automated data structure identification that targets C source code. Our technique first applies a novel abstraction on the evolving memory structures observed at runtime to discover data structure building blocks. By analyzing the interconnections between building blocks we are then able to identify, e.g., binary trees, doubly-linked lists, skip lists, and relationships between these such as nesting. Since the true shape of a data structure may be temporarily obscured by manipulation operations, we ensure robustness by first discovering and then reinforcing evidence for data structure observations. We show the utility of our DSI prototype implementation by applying it to both synthetic and real world examples. DSI outputs summarizations of the identified data structures, which will benefit software developers when maintaining (legacy) code and inform other applications such as memory visualization and program verification.

With the availability of the AUTOSAR standard, model-driven methodologies are becoming established in theautomotive domain. However, the process of creating models ofexisting system components is often difficult and time consuming, especially when legacy code has to be re-used or informationabout the exact timing behavior is needed. In order to tackle thisreverse engineering problem, we present CoreTAna, a novel toolthat derives an AUTOSAR compliant model of a real-time systemfrom a dynamic analysis of its trace recordings. This paper givesan overview of CoreTAna's current features and discusses itsbenefits for reverse engineering.

Abstract This article presents a case study on retrospective verification of the Linux Virtual File System (VFS), which is aimed at checking violations of API usage rules and memory properties. Since VFS maintains dynamic data structures and is written in a mixture of C and inlined assembly, modern software model checkers cannot be applied. Our case study centres around our novel automated software verification tool, the SOCA Verifier, which symbolically executes and analyses compiled code. We describe how this verifier deals with complex features such as memory access, pointer aliasing and computed jumps in the VFS implementation, while reducing manual modelling to a minimum. Our results show that the SOCA Verifier is capable of analysing the complex Linux VFS implementation reliably and efficiently, thereby going beyond traditional testing tools and into niches that current software model checkers do not reach. This testifies to the SOCA Verifier’s suitability as an effective and efficient bug-finding tool during the development of operating system components.

Journal Article To Parallelize or to Optimize? Get access Jonathan Ezekiel, Jonathan Ezekiel Department of Computing, Imperial College, London, UK.E-mail: [email protected] Search for other works by this author on: Oxford Academic Google Scholar Gerald Lüttgen, Gerald Lüttgen Department of Computer Science, University of York, Heslington, York YO10 5DD, UK.E-mail: [email protected] Search for other works by this author on: Oxford Academic Google Scholar Radu Siminiceanu Radu Siminiceanu National Institute of Aerospace, Hampton, Virginia, USA.E-mail: [email protected] Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 21, Issue 1, February 2011, Pages 85–120, https://doi.org/10.1093/logcom/exp006 Published: 12 February 2009 Article history Received: 29 February 2008 Published: 12 February 2009

Reactive controller programming is a difficult and significant task within embedded systems engineering, and is a multi-billion pound business. Despite its importance, surprisingly few books are available on this topic. So this new book by Doron Drusinsky gave me a burst of excitement and hope, and so it should be both for academics who are looking for a good textbook for their students and for engineers who need to get to grips with modern tools for embedded software development. Drusinsky has worked in the industry for many years, mostly on designing statechart-based development tools. A few years ago he took up an academic post and now teaches computer science and software engineering at the Naval Postgraduate School in California. This mix of industrial and academic experience should give Drusinsky just the right background for writing a book on reactive controller programming and verification. However, first things first. The title of the book is somewhat misleading, showing foot stamps of the publisher's marketing department. Drusinsky's book is not about modelling and verification using UML Statecharts, but about programming and verification usingStateRoverTM. StateRover is a graphical programming tool developed by Drusinsky at his Time-Rover company. It supports statecharts and flowcharts for the high-level programming of complex real-time software, automatic Java code generation and run-time verification of temporal assertions. As such, the book employs a new statechart dialect based on UML Statecharts, which has several unique syntactical and semantical features. Drusinsky's book also advocates Statechart Assertions. These allow for writing programs and their desired temporal properties within the same language, although non-determinism is permitted only in the latter. The concept of Statechart Assertions is close to that of observer automata which is deployed in competing design tools, such as Esterel Technologies' SCADETM or Reactive System's REACTIS® Validator for The MathWorks' Simulink/Stateflow® tool. In contrast to these tools, however, StateRover does not support model checking of temporal properties at compile time, but instead supports execution-based model checking at run time or simulation time. Chapter 1 summarizes selected topics of automata and formal language theory, including variants of finite automata and finite state machines, conversions between different kinds of automata and succinctness. Drusinsky attempts to convey these basics to practitioners by adopting some of their language. But is ‘domain of discourse’ really a more comprehensible term for ‘alphabet’? Chapter 2 introduces the statechart dialect implemented in StateRover, illustrates Java code generation from such statecharts, and discusses some non-standard statechart features such as flowchart elements and critical regions. Particular attention is paid to practicality and code generation, rather than to proposing a statechart dialect with a clean semantics. Chapter 3 discusses some ‘academic’ languages for specifying reactive systems. The focus is on temporal logics and their abilities to express real-time constraints in general, and on linear-time temporal logic (LTL) and metric temporal logic (MTL) in particular. The chapter also discusses run-time monitoring and glances at the TemporalRoverTM and DBRoverTM sister tools of StateRover. Chapter 4 presents Statechart Assertions and illustrates how they can be used to specify a variety of temporal properties related to the traffic-light-controller example that is used throughout the book. Drusinsky also shows how Statechart Assertions can be simulated and tested using the JUnit testing framework. Chapter 5 justifies Drusinsky's adoption of Statechart Assertions and run-time model checking for verification. It also gives advice on the process of devising, writing and applying assertions and, equally important, on how to reuse assertions via assertion libraries. Chapter 6 describes a case study of applying StateRover in the context of the U.S. Ballistic Missile Defense Project. This chapter is contributed by Nick Sklavounos who is a key developer within this project. No details of the case study are presented, although there is a useful discussion on the wider project management issues when employing modern software tools such as StateRover. Overall, this book is a brave attempt at addressing a difficult topic, adopting a fresh, pragmatic and illustrative approach. Nevertheless, I am disappointed. Firstly, the book's presentation could easily be much improved by eliminating the many forward and backward references. Secondly, a short introduction to the JUnit testing framework and a good discussion of the literature and related languages and tools would have rounded this book off. Thirdly, spelling out who the intended audience is might have helped the author to write a more focused book. On the one hand, this book is not what I am looking for as an academic textbook. Its technical content is too shallow, often imprecise, and there are too many loose ends. This is because most aspects of reactive controller programming and verification are explained from a tool implementor's point of view. There is no formal treatment of StateRover's semantics, its code-generation facility and its run-time verification engine. All these aspects are introduced in a rather ad hoc manner and refer to ‘implementation semantics’. Without basic knowledge in statecharts and program verification, I feel that parts of the book are difficult to digest. On the other hand, the book also does not give sufficient details for engineers who intend to deploy StateRover in their future projects. They would likely have wished for step-to-step guidelines on the use of StateRover's features and an in-depth case study. I also had expected a trial version of StateRover on the accompanying CD. Despite its shortcomings, I can recommend this book to students as a supplementary textbook, so as to help them relate the theory taught in computing degree courses to software-engineering practice. Some engineers may also find this book a good source for gaining an understanding of run-time verification and of the philosophy behind the StateRover tool.

More than a decade ago, Moller and Tofts published their seminal work on relating processes that are annotated with lower time bounds, with respect to speed. Their paper has left open many questions concerning the semantic theory for their suggested bisimulation–based faster–than preorder, the MT–preorder, which have not been addressed since. The encountered difficulties concern a general compositionality result, a complete axiom system for finite processes, and a convincing intuitive justification of the MT–preorder. This paper solves these difficulties by developing and employing novel tools for reasoning in discrete–time process algebra, in particular a general commutation lemma relating the sequencing of action and clock transitions. Most importantly, it is proved that the MT–preorder is fully–abstract with respect to a natural amortized preorder that uses a simple bookkeeping mechanism for deciding whether one process is faster than another. Together these results reveal the intuitive roots of the MT–preorder as a faster–than relation, while testifying to its semantic elegance. This lifts some of the barriers that have so far hampered progress in semantic theories for comparing the speed of processes. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

No abstract available.

No abstract available.

The semantics of Statecharts macro steps, as introduced by Pnueli and Shalev [1991], lacks compositionality. This article first analyzes the compositionality problem and traces it back to the invalidity of the Law of the Excluded Middle. It then characterizes the semantics via a particular class of linear intuitionistic Kripke models. This yields, for the first time in the literature, a simple fully abstract semantics that interprets Pnueli and Shalev's concept of failure naturally. The results not only give insight into the semantic subtleties of Statecharts, but also provide a basis for an implementation, for developing algebraic theories for macro steps, and for comparing different Statecharts variants.

Statecharts is a visual language for specifying reactive system behavior. The formalism extends traditional finite-state machines with notions of hierarchy and concurrency, and it is used in many popular software design notations. A large part of the appeal of Statecharts derives from its basis in state machines, with their intuitive operational interpretation. The classical semantics of Statecharts, however, suffers from a serious defect; it is not compositional, meaning that the behavior of system descriptions cannot be inferred from the behavior of their subsystems. Compositionality is a prerequisite for exploiting the modular structure of Statecharts for simulation, verification, and code generation, and it also provides the necessary foundation for reusability.

Abstract We present a method for thecompositional constructionof theminimal transition systemthat represents the semantics of a given distributed system. Our aim is to control thestate explosioncaused by the interleavings of actions of communicating parallel components byreduction stepsthat exploitglobalcommunication constraints given in terms ofinterface specifications.Theeffectof the method, which is developed forbisimulation semanticshere, depends on the structure of the distributed system under consideration, and theaccuracyof the interface specifications. However, itscorrectnessis independent of the correctness of the interface specifications provided by the program designer.