Analysis of Properties of Complex Systems with Abstract State Machines

Abstract State Machines (ASMs) represent a general model of computation which combines the two fundamental concepts of transition rule, to model the dynamic aspects of a system, and abstract state, to model the static aspects at any desired level of abstraction. Along the years, ASMs have been successfully applied to the development of critical and complex systems in a wide range of application domains and to the analysis of their computationally interesting properties. However, unlike other wellknown and established formalisms, such as Petri nets, they lack of a framework aimed at better supporting their applicability to the formal verication of systems. The goal of this thesis is to reinforce the ASM formalism as a conceptual tool that developers can nd useful and practical in order to analyze software system properties in an operational fashion. Such properties can be mainly distinguished into two orthogonal classications of properties: domain-independent and domain-specic properties, concerning the application domain, and liveness and safety properties, concerning the computation of the particular system under study. In accordance with these classications, the ìpresent thesis focuses on four properties: starvation-freedom and deadlock-freedom, as instances of domain-independent properties, liveness and safety respectively, and network topology awareness and blackhole-freedom, as instances of domain-specic properties, liveness and safety respectively. The latter are more precisely framed within the context of Mobile Ad-hoc NETworks (MANETs). The contribution of this thesis is manifold. On one hand, this thesis contributes by providing operational characterizations of starvation-freedom and deadlockfreedom in terms of ASMs. Such characterizations are aimed at overcoming the main limitations that penalize traditional manual and automatic verication techniques applied to ASMs. On the other hand, this thesis contributes by showing the versatility of the ASM approach into studying system properties in the particular MANET domain. To this end, the present thesis proposes two variants of the well-known Ad-hoc On-demand Distance Vector (AODV) routing protocol for MANETs, both studied with ASMs. The rst one is aimed at increasing the network topology awareness owned by each node; the second is aimed at intercepting (cooperative) blackhole attacks. In this context, the thesis also contributes by providing for the rst time an executable ASM-based model to evaluate the MANETs' behavior. Finally, in order to deepen into the issues above, this thesis also contributes by proposing the application of predicate abstraction to ASMs.