Spelling suggestions: "subject:"deadline freedom""
1 |
A refinement based strategy for locally verifying networks of CSP processesANTONINO, Pedro Ribeiro Gonçalves 31 March 2014 (has links)
The increase of computer systems complexity has led to a direct increase in the difficulty of
verifying their correctness. For mastering this complexity, formal methods can be used in
the development of systems providing techniques for both design and verification. Regarding
concurrent and distributed systems, the necessity of a formal approach is more prominent given
the substantial increase in complexity due to the countless number of interactions between
their constituent systems. Unfortunately, however, current methods are not capable of dealing
with the automated analysis of such systems in general, even if we consider only classical
properties such as deadlock freedom; the state explosion problem is the main reason for this
ineffectiveness.
This work is a contribution in this direction. Particularly, considering networks of CSP processes,
this work proposes a local strategy for deadlock analysis based on the notion of process
refinement. The locality of this strategy prevents the state explosion problem generated by the
interaction of constituent systems, which represents a major asset of our strategy. We define a
refinement assertion for checking conflict freedom between pairs of processes in the network;
this can be used for the local verification of networks with an acyclic communication topology.
Concerning networks with a cyclic communication topology, we propose three patterns
that prevent deadlocks: the resource allocation, the client/server and the async dynamic. These
patterns impose behavioural and structural restrictions to prevent deadlocks. The behavioural
restrictions are also captured by refinement assertions, which enable one to automatically verify
these conditions using a refinement checker.
Besides this, we develop four case studies to evaluate the efficiency of our strategy in practice:
a ring buffer, a dining philosopher, and two variations of a leadership election algorithm.
One of the variations of the leadership election algorithm consists of a model used in practice by
the B&O Company, an industrial partner. In this study, we compare our strategy with two other
techniques for deadlock freedom verification, the SSD algorithm of the Deadlock Checker tool
and the built-in deadlock freedom assertion of FDR. This study demonstrates how our strategy
can be used and that it might be a useful alternative to analysing complex industrial systems for
deadlock freedom. / Submitted by Luiz Felipe Barbosa (luiz.fbabreu2@ufpe.br) on 2015-03-10T16:54:41Z
No. of bitstreams: 2
DISSERTAÇÃO Pedro Ribeiro Gonçalves Antônio.pdf: 921372 bytes, checksum: 64def1c3ae98cbca7868d944c1f786f2 (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-11T17:34:41Z (GMT). No. of bitstreams: 2
DISSERTAÇÃO Pedro Ribeiro Gonçalves Antônio.pdf: 921372 bytes, checksum: 64def1c3ae98cbca7868d944c1f786f2 (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5)
Previous issue date: 2014-03-31 / Com o aumento da complexidade dos sistemas computacionais, houve também um aumento da
dificuldade na tarefa de verificação de sistemas. Para lidar com essa complexidade, métodos
formais podem ser usados no desenvolvimento de sistemas, fornecendo técnicas para a modelagem
e verificação. No contexto de sistemas concorrentes e distribuídos, a necessidade de uma
abordagem formal é ainda mais proeminente, dadas as inúmeras possibilidades de interação entre
seus sistemas componentes. Entretanto, infelizmente, os métodos atuais não se encontram,
de forma geral, completamente aptos a lidar com a análise automática desses sistemas, mesmo
em se tratando de propriedades clássicas como a ausência de deadlocks. A explosão do espaço
de estados a ser analisado é o principal fator para essa ineficácia por parte desses sistemas.
O trabalho apresentado é uma contribuição nesta direção. Considerando o conceito de redes
de processos CSP, o presente trabalho propõe uma estratégia local para a análise de deadlocks
baseada na noção de refinamento de processos. A localidade dessa estratégia previne a explosão
de espaço de estados causada pela interação de sistemas componentes, o que constitui uma
vantajosa característica da nossa estratégia. O trabalho define uma expressão de refinamento
capturando o conceito de ausência de conflito, que pode ser usado para verificar localmente que
uma rede de processos com uma topologia de comunicação acíclica é livre de deadlocks. Para
as redes com topologia cíclica, o trabalho sistematiza e formaliza três padrões comportamentais
que impedem deadlocks: o alocação de recursos, o cliente/servidor e o assíncrono dinâmico.
Esses padrões impõem restrições comportamentais e estruturais para prevenir deadlocks. Essas
restrições comportamentais também são capturadas através de expressões de refinamento,
o que possibilita a verificação automática dessas condições com o uso de um verificador de
refinamento.
Além disso, são apresentados quatro estudos de caso usados para avaliar o desempenho da
nossa técnica na prática: um buffer circular, um jantar dos filósofos e duas variações de um
algoritmo para eleição de líder. Uma dessas variações consiste num modelo usado na prática
pela empresa B&O, um parceiro industrial. Nesse estudo, avaliamos a nossa técnica em comparação
com outras duas técnicas para verificação de ausência de deadlocks, o algoritmo SSD
da ferramenta Deadlock Checker e a asserção de verificação de deadlocks padrão do verificador
de modelos FDR. Esse estudo demonstra como a nossa estratégia é aplicada e que ela pode ser
uma alternativa vantajosa para a verificação de sistemas complexos.
|
2 |
Behavioral service substitutionParnjai, Jarungjit 22 April 2013 (has links)
Serviceevolution erlaubt es, einen Service durch einen anderen Service zu verfeinern oder zu ersetzen. Der Austausch durch einen anderen Service sollte garantieren, dass alle oder ausgewählte Partner des Originalservices erhalten bleiben. In dieser Arbeit entwickeln wir einen Ansatz welcher einem Serviceentwickler helfen soll, Analyse- und Syntheseaufgaben für den Serviceaustausch so durchzuführen, dass jeder Partner eines gegebenen Services beim Austausch erhalten bleibt. Wir modellieren einen Kontrollfluss eines Services als Beschreibung der Reihenfolge von asynchron kommunizierenden Ereignissen mittels eines impliziten ungeordneten Nachrichtenspeichers. Weiterhin studieren wir den Verhaltensaspekt von korrekter Interaktion zwischen Services und konzentrieren uns auf zwei Varianten von Verklemmungsfreiheit als Korrektheitskriterien von Serviceersetzung. Der wichtigste Beitrag ist ein Ansatz zur Charakterisierung jedes möglichen Austausches eines gegebenen Services. Die zentrale Idee dieses Ansatzes ist eine systematische Untersuchung der Verbindung zwischen einem Service und all seiner Partner bzgl. eines gegebenen Korrektheitskriteriums. Wir nutzen diese Verbindung um von einem gegebenen Service einen kanonischen Partner und einen kanonischen Austausch bzgl. aller Partner zu synthetisieren. Ein Service welcher den kanonischen Austausch eines gegebenen Services verfeinert wird als Austausch des gegebenen Services angesehen, wenn die Menge all seiner Partner jeden Partner des gegebenen Services enthält. Mit dem kanonischen Austausch eines gegebenen Services identifizieren wir die Menge der möglichen austauschenden Services eines gegebenen Services bei der jeder exakt die gleichen Partner wie der gegebene Service hat. Einige Ergebnisse dieser Arbeit fundieren auf früheren Arbeiten zu Austausch und Korrektheit von Services und können daher mit diesen verbunden werden um schwierigere Analyse- und Syntheseaufgaben für den Serviceaustausch durchzuführen. / Service evolution allows one service to be refined into or substituted by another service. Substituting one service by another service should guarantee to preserve all or selected partners of the original service. In this thesis, we develop an approach that shall assist a service designer, such as a domain expert, to perform analysis and synthesis tasks on service substitution. We model a control flow of services that describes the ordering of asynchronously communicating events over an implicit unordered message buffer. We study the behavioral aspect of correct interaction between services and concentrate on two variants of deadlock freedom as correctness criteria of service substitution. The major contribution of this thesis is an approach for characterizing the set of all substitutes for a given service. We systematically investigate the relationship between a service and all its partners under a given correctness criterion and employ this relationship to synthesize from a given service its canonical partner and its canonical substitute with respect to all partners. A service that refines the canonical substitute for a given service is regarded as a substitute for the given service if the set of all its partners includes every partner of the given service. With the canonical substitute of a given service, we identify a specific subset of the set of all substitutes for the given service, each of which has exactly the same set of partners as that of the given service. Parts of the results in this thesis have been established upon previous works on service substitution and correctness of services. Consequently, we can also combine our results with the related existing techniques to perform more sophisticated analysis and synthesis tasks on service substitution.
|
Page generated in 0.031 seconds