Temporal assertions for sequential and concurrent programs [Elektronische Ressource] / Volker Stolz. [RWTH Aachen, Department of Computer Science]

Sujets

• Informatik

Informations

• Publié par: rheinisch-westfalischen_technischen_hochschule_-rwth-_aachen
• Publié le: 01 janvier 2007
• Nombre de lectures: 13
• Langue: English

Extrait

Aachen
Department of Computer Science
Technical Report
TemporalAssertions forSequentialandCon-
current Programs
Volker Stolz
ISSN 0935–3232 · Aachener Informatik Berichte · AIB-2007-15
RWTH Aachen · Department of Computer Science · August 2007The publications of the Department of Computer Science of RWTH Aachen (Aachen
University of Technology) are in general accessible through the World Wide Web.
http://aib.informatik.rwth-aachen.de/Temporal Assertions for Sequential and
Concurrent Programs
Von der Fakult¨ at fur¨ Mathematik, Informatik und
Naturwissenschaften der Rheinisch-Westf¨alischen
Technischen Hochschule Aachen zur Erlangung des
akademischen Grades eines Doktors der
Naturwissenschaften genehmigte Dissertation
vorgelegt von
Diplom-Informatiker
Volker Stolz
aus
W¨ urselen
Berichter: Prof. em. Dr. Klaus Indermark
Prof. Bernd Finkbeiner, Ph. D.
Tag der mundlic¨ hen Prufung:¨ 20.7.2006
Diese Dissertation ist auf den Internetseiten der Hochschulbibliothek online verfug¨ bar.Temporal Assertions for Sequential and
Concurrent Programs
Dipl.-Inform. Volker Stolz
Abstract
In this thesis, we present an extension to the well-known concept of assertions:
temporal assertions allow the specification and validation of modal safety properties
of an application at runtime. We see this as a necessary step in enforcing the growing
number of implicit requirements of software specifications, which are often only
informally defined in the documentation of application program interfaces (API)
and are beyond the reach of type checkers, compilers, or model checkers. Also, we
show how our techniques can be applied to existing programs without modifying
the source code. Although, like assertions, our approach cannot prove the absence
of errors, it gives the programmer a more powerful means of automatically checking
assumptions about his program at runtime.
It can also be used to look for behaviour that indicates the potential for problems,
that is, that might be used to predict future errors. An example is the Lock-order
Reversal pattern which indicates a potential deadlock in a concurrent program.
Our parametrised propositions approach gives us a convenient way to handle dy-
namic systems: in real-world programs, almost always dynamic data is used, for
example, new objects are instantiated, or new threads created. While there is al-
ready a plethora of work on checking some properties of those systems, they are
usually concerned with the boundedness of the number of resources, and not nec-
essarily with the interaction of those objects. Especially, they are often limited to
either non-recursive examples or some coarse finite abstraction.
Propositions in our practical examples are certain events which we can observe in
the execution of a program: method invocation with caller/callee and arguments,
object attribute access, or actions related to concurrency.
If we have a property which has to be checked on a per-object basis (that is,
instantiated for each object or set of objects), our template mechanism dynamically
instantiates a given formula based on observers, so-called existence predicates.In
a static approach, this would have to be solved by generating all instances of the
property beforehand and checking each of them against the model, leading again to
a finitary abstraction.
As application, we see two kinds of properties: firstly, properties over the universalbehaviour of data structures. For example, it universally holds that a pop from a
stack should not be performed unless something has actually been pushed onto
it. Data structures and their respective functionality are usually accumulated in
libraries. Thus, a test facility implemented in the library should be available to any
application using it. Furthermore, the corresponding formula can be used very much
like a design pattern from Software Engineering and new implementations of some
previously specified behaviour can be checked against the temporal specification of
the pattern.
Secondly, there are application specific properties. These can be based, for exam-
ple, on the specification that defined the application. Or they can be derived from
informal requirements, stated in the documentation. Rather than being invariants
of a structure like above, they may not be evident and need to be “developed”
as much as the source code for the application has to be developed. As a lot of
current research also focuses on documenting and enforcing such specifications, we
later comment on the necessity and advantages of storing such semantic annotations
about the application in a machine-readable format.
Naturally, the additional level of possible checks comes at a penalty: runtime
overhead. In the most general case, for every event, the set of affected state ma-
chines (the automaton-based representation of the property) must be determined.
This also includes possibly instantiating new ones. Then, in each machine, a state
transition must be triggered. As the underlying framework of our mechanism is
based on alternating finite automata, we already incur an exponential blow-up in
the size of the automaton when moving to nondeterministic automata. The addi-
tional determinisation of said nondeterministic automata will make this approach
infeasible in practice.
Instead, we will resolve the nondeterminism at runtime at the cost of performance:
after statically generating an alternating finite automaton from the formula and
eventually pre-calculating the (nondeterministic) outgoing edges for each state, we
use a breadth-first approach over the branches for checking the acceptance condition
of the input. We will see that this solution has double-exponential overhead, but
we still consider it as a useful tool, since the average behaviour might prove not to
be as harsh as this complexity might suggest. Also, using our algorithm offline, on
a recorded trace, is an option that does not slow down the actual application.
Practical examples from object-based and concurrent programs written inHaskell,
C,and Java underline the general usefulness of the approach. A proof-of-concept
prototype developed in Java confirmed the practicality of our approach.Acknowledgments
My sincerest thanks go to my supervisor Prof. Dr. Klaus Indermark, who
gave me the opportunity as a teaching and research assistant to find my
bearings in a rapidly advancing scientific world. His rigorous lectures on
subjects that elsewhere are only taught as practical courses will sorely
be missed.
I thank Prof. Bernd Finkbeiner, Ph. D., for kindly agreeing to be a
member on the examination board.
I am indebted to Prof. Dr. Ir. Joost-Pieter Katoen, who, after taking over
I2, provided unquestioned infrastructural support until this thesis could
be finished and whose activism provided many additional last-minute
insights into formal methods.
Both old and new colleagues at I2 formed an amiable group that made
our department a pleasurable place to work on a day to day basis. I shall
miss the friendly environment and their helpful contributions.
As for my office mate and invaluable friend Dr. Michael Weber, his suf-
fering for (willingly or unwillingly) participating in my research and soft-
ware development should not be underestimated. Thank you!
Finally, I also thank my friends in Aachen and abroad, for all their advice
and making sure that there is in fact life outside of The Thesis.
Volker Stolz
Aachen, May 2006Contents
1 Introduction 1
1.1 RuntimeVerification ......... ........... ....... 1
1.2 ModelChecking . ........... 3
1.3 TemporalAssertions ....... 4
1.4 Outline...... 6
2 Reasoning about Programs 7
2.1 PropertiesofPrograms ........ ........... ....... 7
2.2 AnObject-basedProgrammingLanguage......... 9
2.3 ExecutionSemantics ......... ....... 13
2.4 StaticAnalysis . ........... 17
2.5 Assertions .... ........... ....... 19
2.6 ExtensiontoConcurrency ...... 19
2.7 ObtainingaTraceModel....... ....... 23
3 Parametrised LTL Formulae 27
3.1 LTL ....... ........... ........... ....... 27
3.2 ExtensiontoParametrisedPropositionsandtheirSemantics ..... 30
3.2.1 VariablesandtheirDomains . ....... 33
3.2.2 ParametrisedPropositions . . 35
3.2.3 Negation in pLTL ...... ........... ....... 44
3.3 Predicates .... ........... 47
3.4 TranslatingLTLFormulaeintoAlternatingFiniteAutomata ..... 50
3.5 ParametrisedAutomatonConstruction .......... ....... 56
3.5.1 HandlingQuantifiedPropositions ......... 56
3.5.2 ParametrisedAutomaton... ........... ....... 60
3.6 AlternativeApproaches........ 73
4 Evaluating Parametrised Formulae at Runtime 77
4.1 TraceExtraction ........... ........... ....... 77
4.2 Example: Lock-orderReversal .... 80
5 Applications and Implementations 87
5.1 GeneralRemarks ........... ........... ....... 87
5.2 RuntimeVerificationofConcurrentHaskellPrograms . . 89
5.3 Cprogramsandcompiledprograms. ....... 92ii Contents
5.4 Instrumenting Javaprograms .......... ........... . 96
5.5 UsingMetadatatoRecordSemanticWisdom . . 99
6 Conclusion 101
6.1 RelatedWork ........ ........... ........... .101
6.2 Summary .......... .107