Abstract: The mathematical notation of formal verification tools do not prevent us from wrongly defining the behaviour of systems, any better than CASE tools do. However, the languages used to build models in the former have precise information which allows us to find errors by means of automatic verification algorithms, e.g. Model Checking, which is not the case in the latter. CASE tools are considered to be user-friendly because of their graphical representation and their 'capability' to provide free textual information to describe constraints not captured either by diagrams or constraint languages (for instance OCL). Thus, CASE tools lack the necessary apparatus to perform (semi-)automatic processing over models.
With software rapidly growing in size and complexity due to new demands, graphical specifications in languages like UML need to be formally verified, before the implementation phase, in order to guarantee the development of more reliable systems. A few years ago, the formal verification community began investigating mechanisms to approximate such graphical specifications to verification tools. While this enterprise had reasonable success on the translation of simple diagrams to Model Checkers' textual input, thus far no better ways of explaining the outcome of such tools have been found. Interpreting the results of verification is still highly human-dependent, and the intensive use of these tools in software development is yet to be achieved.
In this talk we propose that a protocol interface joining both technologies can be a more reliable solution to bridging this gap. First, it would avoid the introduction of notation overhead on either side. Second, we would be able to implement algorihms for reasoning about the relationships between high level specifications and their verification, and also for guiding the verification and result's explanation with an AI agent "flavour".
Biography:
Senior Lecturer
Department of Computer Science
Federal University of Amazonas - Manaus - Brazil
Current Duties: