Towards the modelling of secure pervasive computing systems: A paradigm of Context-Aware Secure Action System

• Propose CASAS, a paradigm for modelling secure pervasive computing systems.
• Present the syntax and a formal semantics for CASAS.
• Present an algorithm for checking system consistency statically (i.e. at compile time).
• Define a set of operators for building complex CASAS systems from simpler ones in a compositional manner.
• Demonstrate the pragmatics of the proposed formalism using a number of real-world case studies.

The design of security-critical pervasive systems is challenging due to that security constraints are often highly dependent on dynamically changing contexts. To increase the trustworthiness of pervasive systems, a dependable approach to system development must be followed, which enables seamless integration of the functional, security and context-awareness requirements. This paper proposes a paradigm which enables the specification of the functional, security and context-awareness requirements of a system in a single formalism, called Context-Aware Secure Action System (CASAS). Its syntax, formal semantics and pragmatics are presented, as well as algorithms and techniques for analysing the behaviour of a pervasive computing system.