Formal Modelling and Verification of Trust in a Pervasive Application

This report is deliverable WP4-01 of the project “Trusted Software Agents and Services for Pervasive Information Environments.” The deliverable reports on the activities of formal modelling and verification of a pervasive application which follows from previous results in the project. The pervasive application is based on several pervasive scenarios already devised and is centred on the user location. This location-based system is first architecturally simplified, while trust requirements are derived from the Trust Analysis Framework presented in the deliverable WP2-01. This first abstraction is then completed by formal modelling of the system in the B formal method. These models enable us to clarify the decision decisions leading to fulfil the trust requirements. We show that the system policy structure is influenced by the priorities given to the system operations and that a sufficiently high level of abstraction is required to model trust properties. The modelling activity is completed by formal verification using the ProB model-checker to automate part of this process. Several models are checked successfully, while detection of errors in other models enables us to understand better the behaviour of the system. In particular, issues relative to the dynamicity of modelled elements are highlighted. The overall methodology followed during these activities proved useful at helping us specifying accurately the trust requirements, so that the pervasive application can be completed in consequence, and is as follows: 1) Model important features of the system First vaguely type the variables; then write a set of operations corresponding to complementary features while (possibly) modifying the variable types to ease this writing; consider the variables by group of similar dynamic properties; 2a) Model-check the model 2a.a) Property violation detected Examine the various aspects of the model (variables, enabled operations, history of operations) to see what part of the property is “false”; Correct the model accordingly; 2a.b) No property violation detected Go back to 2a until coverage rate is enough; possible changes to the model include: modify the initialisation to test other situations (in B use “choice by predicate”); add inconsistencies in the model; 2b) Animate the model 2b.a) Execute the desired sequence of operations (validation); 2b.b) Find an interesting state, then 2a.a or 2a.b applies; 2b.c) Backtrack from a state where the invariant is violated; 3) Go back to 1 (complete the model) or refine the model.