Subsequence invariants [Elektronische Ressource] / Klaus Dräger
112 Pages

Subsequence invariants [Elektronische Ressource] / Klaus Dräger

Downloading requires you to have access to the YouScribe library
Learn all about the services we offer


Subsequence InvariantsDissertation zur Erlangung des Grades des Doktors der Naturwissenschaften derNaturwissenschaftlich-Technischen Fakulta¨ten der Universit¨at des SaarlandesKlaus Dr¨agerSaarbru¨cken, 2010Tag des Kolloquiums 23.08.2010Dekan Prof. Dr. Holger HermannsPru¨fungsausschussVorsitzender Prof. Dr. Reinhard WilhelmBerichterstattende Prof. Dr. Bernd FinkbeinerProf. Dr. Ernst-Ru¨diger OlderogProf. Dr. Andreas PodelskiAkademischer Mitarbeiter Dr. Thomas HillenbrandiAbstractIn this thesis, we introduce subsequence invariants, a new class of invariantsfor the specification and verification of systems. Unlike state invariants, whichrefer to the state variables of the system, subsequence invariants characterizethe behavior of a concurrent system in terms of the occurrences of sequences ofsynchronization events.The first type of such invariants, pure subsequence invariants, are linearconstraints over the possible numbers of such occurrences, where we allow everyoccurrence of a subsequence to be interleaved arbitrarily with other events. Wethen describe the more general class of phased subsequence invariants, in whichadditionalrestrictionscanbeplacedontheeventsthatmayoccurbetweenthoseof a given sequence. In either case, subsequence invariants are preserved whena given process is composed with additional processes. subsequence invariantscan therefore be computed individually for each process and then be used toreason about the full system.



Published by
Published 01 January 2010
Reads 696
Language English