Enabling Reasoning And Verification Support For Intelligent Agent Systems, Using Formal Methods

Abstract

Formal methods are techniques, languages and tools based on mathematics, which provide an unambiguous, strict mathematical description or specification which is used for effective design, analysis and verification of desired properties of the system. An important branch of formal methods are algebraic specification languages with a rigorous basis on mathematical logical systems or combinations of them. Such a language is CafeOBJ, an executable, new generation algebraic specification language, member of the OBJ family languages. Its main characteristic, that differentiates it from other formalisms, is its direct support to behavioural specification paradigm since it embeds special hidden sorts and behavioural operators in its syntax. Behavioural specification is based on hidden algebra and supports an object oriented style of algebraic specification. It also supports specification of distributed complex systems as abstract state machines and verification of safety properties of them through theorem proving techniques such as simultaneous induction and coinduction. The scope of the thesis is the modelling and verification of intelligent agents using algebraic specification techniques. By intelligent agents we refer to the systems used in the New or Semantic Web in order to achieve the need for reactivity, interaction and communication between its various components. An intelligent agent can be defined as an autonomous entity which observes through sensors and acts upon an environment using actuators (i.e. it is an agent) and directs its activity towards achieving goals. Due to the special characteristics of such systems, and their increased development as well as their use in critical domains, the requirements for reliability, security and proper functionality has led to the use of formal methods for their analysis and the development of new methodologies oriented to these systems. To this end, in this thesis an algebraic framework is proposed for the specification and verification of two basic types of intelligent systems, those whose behaviour is expressed in terms of reactive rules (reactive rule-based systems) and those who can sense the changes in their physical environment (context-aware systems), and adapt their behaviour accordingly. In the first category of intelligent agents, we first give formal semantics, based on the hidden algebra formalism, to the basic reactive rule families, then we formally analyse and verify reactive rule-based systems using equational logic, next we propose the use of rewriting logic for the detection of structural errors of the rules, such as termination and conuence, and finally we compare the proposed approaches. In the second type of agents, which are usually more complex, the specification of the system, is defined as the composition of the specifications of3its components, i.e. the specifications which describe data types as visible sorts and the various components of the system as Observational Transition Systems, a kind of behavioural object. In this way the complex interactions of such systems can be expressed in a natural and dynamic way. Based on the specification, verification of properties of the intelligent system using theorem proving techniques is also feasible. The fact that the system is specified as a transition system, using equational or rewriting logic, makes the method easier to read, understand and learn than other related methods, which prerequisite deeper knowledge of theorem proving, or that are based in higher order logic for example. To demonstrate the applicability and effectiveness of the proposed methodologies, a number of case studies are conducted. Security aspects of intelligent systems are of major importance, and it was inevitable to take them into account. To this end we present the verification of the behaviour of various intelligent systems from the literature. In the last section of the thesis, an extension of the specification and verification methodology, supported by the CafeOBJ language, is proposed that provides more automation for the proofs and allows the use of more conventional verification tools, by integrating it with the Athena automated theorem proving system. The proposed methodology is based on the interaction of the two languages so as to be able to exploit the nice properties of each method and thus have better results in the verification process. Finally, a number of applications of the methodology in protocols that are often used as case studies, especially for tools dedicated to the verification of complex systems, are presented.