Subsequence invariants [Elektronische Ressource] / Klaus Dräger

Description

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.

Sujets

• Informatik

Informations

• Publié par: universitat_des_saarlandes
• Publié le: 01 janvier 2010
• Nombre de lectures: 696
• Langue: English

Extrait