1. Inicio
  2. Atrás
Título: Verifying finite-state properties of large-scale programs
Autores: Bodden, Eric
Fecha: 2010
Publicador: McGill University - MCGILL
Fuente:
Tipo: Electronic Thesis or Dissertation
Tema: Applied Sciences - Computer Science
Descripción: Designers of software components can use finite-state properties to denote behavioral interface specifications which enforce client-side programming rules that state how the components ought to be used. This allows users of these components to check their client code for compliance with these rules, both statically and at runtime.
In this dissertation we explain the design and implementation of Clara, a framework for specifying and verifying finite-state properties of large-scale programs. With Clara, programmers specify finite-state properties together with runtime monitors, using a syntactic extension to the aspect-oriented programming language AspectJ. Clara then uses a sequence of three increasingly detailed static analyses to determine if the program satisfies the finite-state properties, i.e., is free of property violations.
Clara produces a list of program points at which the program may violate the properties, ranked by a confidence value. If violations are possible, Clara also instruments the program with the supplied runtime monitor, which will capture property violations when the program executes. Due to its static analyses, Clara can omit the instrumentation at program locations which the analyses proved safe, and so optimize the instrumented program. When much instrumentation remains, Clara partitions the instrumentation into subsets, so that one can distribute multiple partially instrumented program versions that each run with a low overhead.
We validated the approach by applying Clara to finite-state properties denoted in multiple formalisms over several large-scale Java programs. Clara proved that most of the programs fulfill our example properties. For most other programs, Clara could remove the monitoring overhead to below 10%. We also found multiple property violations by manually inspecting the top entries in Clara's ranked result list.
Les concepteurs des différentes composantes logicielles peuvent utiliser les propriétés des automates finis pour fixer les spécifications de l'interface comportementale qui contrôleront les règles de programmations définissant l'utilisation des composantes. Ceci permet aux utilisateurs de ces composantes de vérifier le respect de ses règles par leurs codes sources, à la fois lors d'une analyse statique qu'à l'exécution.
Dans cette dissertation, nous montrerons la conception de Clara, une structure qui permet de spécifier et de vérifier les propriétés des automates finis dans des programmes étendus, puis expliquerons son implantation. Le programmeur, à l'aide de Clara, peut définir les propriétés des automates finis en complément aux processus de vérification à l'exécution, en utilisant une extension de la syntaxe d'AspectJ, un langage de programmation orienté aspect. Clara utilise alors, en séquence, trois analyses statiques de précision croissante pour déterminer si le programme respecte les propriétés des automates finis.
Clara produit une liste des positions dans le code source où il y a risque de violation de ces «propriétés», en ordre décroissant de certitude d'une violation. Quand cela est possible, Clara ajoute au programme des processus de vérification permettant d'étudier la violation de «propriétés» lors de son exécution. Grâce à son analyse statique, Clara n'ajoute pas au code ces processus dans les portions de code qui n'ont pas la possibilité de violer les propriétés des automates finis, ce qui limite les ralentissements dus aux processus de vérification. Lorsque ses ajouts restent considérables, Clara organise les processus de vérification à l'exécution en sous-groupe, de sorte qu'il soit possible de distribuer différentes versions du programme contenant seulement une partie de ceux-ci, limitant ainsi l'utilisation des ressources système à l'exécution.
Nous avons validé cette approche en soumettant à Clara les propriétés des automates finis sous différents modèles à appliquer sur différents programmes Java. Clara a permis de prouver que la plupart de ces programmes respectaient déjà les propriétés définies. Dans les autres cas, Clara a pu réduire le coût des processus de vérification à moins de 10%. De plus, nous avons pu localiser de nombreuses violations de propriété manuellement, en inspectant les entrées en importance dans la liste produite par Clara.
Idioma: en