Catálogo de publicaciones - libros

The Live Sequence Charts (LSC) language is a formally rigorous variant of the well-known scenario language Message Sequence Charts (MSC). LSCs yield expressive power by means to distinguish mandatory and scenario behaviour, means to characterise by another scenario the context in which a specification applies, and means to distinguish required from possible progress, i.e. to require liveness.

From the original proposal by Damm & Harel [1], two slightly different dialects emerged, one in the context of LSC play-in and -out [2] and one for the use of LSCs as formal requirements specification language in formal, model-based approaches to software development [3].

In this paper, we investigate the expressive power of LSCs in the sense of [3]. That is, we first (constructively) show that for each LSC there is an equivalent CTL formula. Complementing existing work, we show that the containment is strict, that is, not each CTL formula has an equivalent LSC. To complete the discussion, we present for the first time a way back, from a syntactically characterised fragment of CTL to the subset of bonded LSC specifications, thereby establishing an equivalence.

In earlier work, we presented an abstraction-refinement mechanism that was successful in verifying automatically the partial correctness of list reversal when applied to an acyclic linked list [10]. This paper reports on the automatic verification of the (partial correctness and termination) of the same list-reversal algorithm, when applied to a linked list. A key contribution that made this result possible is an extension of the technique [14] to enable the maintenance of reachability information for a restricted class of possibly-cyclic data structures, which includes possibly-cyclic linked lists.

Counterexample-guided abstraction refinement (CEGAR) is a powerful technique to scale automatic program analysis techniques to large programs. However, so far it has been used primarily for model checking in the context of predicate abstraction. We formalize CEGAR for general powerset domains. If a spurious abstract counterexample needs to be removed through abstraction refinement, there are often several choices, such as which program location(s) to refine, which abstract domain(s) to use at different locations, and which abstract values to compute. We define several plausible preference orderings on abstraction refinements, such as refining as “late” as possible and as “coarse” as possible. We present generic algorithms for finding refinements that are optimal with respect to the different preference orderings. We also compare the different orderings with respect to desirable properties, including the property if locally optimal refinements compose to a global optimum. Finally, we point out some difficulties with CEGAR for non-powerset domains.

Control flow analysis is a powerful method for analysing which functions are applied to which arguments. However, many users find the information more understandable if the information is presented in the form of types rather than sets of function abstractions. We therefore show how to translate the result of the control flow analysis into the syntax of types (to be called ).

To compare our approach with the more traditional approach using type systems (to be called ) we develop the subtyping relations in both approaches; in particular we show that covariant subtyping is the appropriate choice for observed types whereas contravariant subtyping is appropriate choice for inferred types. This serves as a technical underpinning of our main thesis that observed types should merely record how the entity in the program at hand whereas inferred types should indicate how the entity in all possible contexts.

Data Flow Analysis as expressed by Monotone Frameworks is often associated with classical imperative programming languages and has played a crucial role in the efficient implementation of these languages. Robin Milner’s Calculus of Communicating Systems, CCS, is concerned with modelling concurrent systems and has mainly been analysed using types and control flow analyses. In the present paper we present an instance of a Monotone Framework together with a novel worklist algorithm for more precisely approximating the flow-sensitive control structure of even infinitary processes expressed in CCS.

Modulo scheduling is a major optimization of high performance compilers wherein The body of a loop is replaced by an overlapping of instructions from different iterations. Hence the compiler can schedule more instructions in parallel than in the original option. Modulo scheduling, being a scheduling optimization, is a typical backend optimization relying on detailed description of the underlying CPU and its instructions to produce a good schedule. This work considers the problem of applying modulo scheduling at source level as a loop transformation, using only general information of the underlying CPU architecture. By doing so it is possible: a) Create a more retargeble compiler as modulo scheduling is now applied at source level, b) Study possible interactions between modulo scheduling and common loop transformations. c) Obtain a source level optimizer whose output is readable to the programmer, yet its final output can be efficiently compiled by a relatively “simple” compiler.

Experimental results show that source level modulo scheduling can improve performance also when low level modulo scheduling is applied by the final compiler, indicating that high level modulo scheduling and low level modulo scheduling can co-exist to improve performance. An algorithm for source level modulo scheduling modifying the abstract syntax tree of a program is presented. This algorithm has been implemented in an automatic parallelizer (Tiny). Preliminary experiments yield runtime and power improvements also for the ARM CPU for embedded systems.