Invited Talks

AAAI Conferences

The need to reduce cost and the desire to tackle ambitious exploration goals pushes NASA toward adopting ever more sophisticated and autonomous software systems for its missions. The techniques of artificial intelligence promise to solve several key problems in the design and implementation of such software. However, the increase in complexity produces legitimate concerns on system correctness, robustness and reliability. While AI has typically strived to demonstrate sophisticated capabilities, not much attention has been given until now to the problems of verification and validation. Remote Agent was the first autonomy architecture to operate in interplanetary space, controlling the Deep Space One spacecraft for a total of 2 days in May 1999.


Formal Software Development in the Verification Support Environment (VSE)

AAAI Conferences

The paper presents a survey of the VSE system, a kind of CASEtool for formal software development. It is a summary of a tutorial presentation describing methodology, formalisms, architecture, and proof support of the system. For illustration a commercial application from the ITsecurity domain is used.


Validation Method for Intelligent Systems

AAAI Conferences

However, when intelligent methods are used in real applications, it is an important problem to validate that both optimality and response time are at expert level. Turing Test approaches are useful in validating intelligent systems. Nevertheless, validation burdens experts with heavy tasks. In distribution mute scheduling, for instance, validation load is considerable since patterns of distribution spots are numerous. A bidirectional, many-sided explanation typed multi-step validation method, which enables to share the validation tasks among experts, KEs and computers, is proposed to diminish the load on busy experts, for validating intelligent systems.


Modelling, Specification and Verification of an Emergency Closing System

AAAI Conferences

In this paper we present a realtime modelling technique which is based on a global clock architecture with a discrete time scale. We argue that this model can be applied to a wide range of scenarios. Furthermore we illustrate the modelling technique by an example describing an emergency closing system which is specified in the VSE tool (Hutter et al. 1999; Rock, Stephan, and Wolpers 1997; 1999).


Verification of Cooperating Systems An Approach Based on Formal Languages

AAAI Conferences

Behaviour of systems is described by formal languages: the sets of all sequences of actions. Regarding abstraction, alphabetic language homomorphisms are used to compute abstract behaviours. To avoid loss of important information when moving to the abstract level, abstracting homomorphisms have to satisfy a certain property called simplicity on the concrete (i.e.


A Case Study in the Mechanical Verification of Fault Tolerance

AAAI Conferences

To date, there is little evidence that modular reasoning about fault-tolerant systems can simplify the verification process in practice. We study this question using a prominent example from the fault tolerance literature: the problem of reliable broadcast in point-to-point networks opposed to crash failures of processes. The experiences from this case study show how modular specification techniques and rigorous proof reuse can indeed help in such undertakings.


The Use of Formal Methods for Trusted Digital Signature Devices

AAAI Conferences

This paper presents a formal security policy model for Smart-Cards with digital signature application. This kind of model is necessary for each evaluation according to Information Technology Security Evaluation Criteria assurance level E4 (Common Criteria level EAL5) and above. Furthermore, we argue that such a model is essential for reasoning about the security of Information Technology components like a specific IT product or IT system. Without an unambiguous definition of what security means, it is impossible to say whether a product really is secure.


Towards Validation of Rule-Based Systems - The Loop is Closed

AAAI Conferences

Thus, the only way to validate these systems is to confront the system with representative test cases and to compare the system's answers with the answers of human experts.


TIC - A Toolkit for Validation in Formal Language Learning

AAAI Conferences

However it seems not an easy task to verify that the modifications are indeed helpful. This is made more complicated through various additional influences inherent in different application domains. In order to obtain a faithful impression of phenomena that are intrinsic to the algorithms, the role of specific domains should be minimized. Our validation toolkit TIC allows to explore the behaviour of various algorithms for learning formal languages. This is a well-examined and standardized application domain.