Formal specification and verification

This activity focuses on the formal specification of smart environments and pervasive healthcare applications.

We adopt formal methods, which are well known techniques able to increase dependability by eliminating errors at the requirement specification and early design stages of the development. We
also use formal methods for runtime verification; that is, the prototype system is monitored while it is running and checked against properties of interest (correctness properties) specified in a formal notation, so that, whenever a violation of correctness properties is detected, a recovery strategy is triggered.

Among the formal methods, we chose Ambient Calculus that is a theoretical framework to model and analyze mobile agent based applications and pervasive systems.

Selected publications

  • A. Coronato and G. De Pietro. 2011. Formal Specification and Verification of Ubiquitous and Pervasive Systems. ACM Transactions on Autonomous and Adaptive Systems, 6, 1, Article 12 (February 2011). ISI Impact Factor (2009): 1.364
  • Antonio Coronato, Giuseppe De Pietro. 2010. Formal Design of Ambient Intelligence Applications. Computer, pp. 60-68, (December 2010) ISI Impact Factor (2009): 2.205
  • Coronato, A. and De Pietro, G. 2010. Formal specification of wireless and pervasive healthcare applications. ACM Transactions on Embedded Computing Systems, 10, 1, Article 12 (August 2010). ISI Impact Factor (2009): 1.099
  • A. Coronato, G. De Pietro, J. H. Park, H. C. Chao. 2010. A Framework for Engineering Pervasive Applications applied to Intra-Vehicular Sensor Network Applications. ACM/Springer MONET Journal, Vol. 15, N. 1 / February, 2010 Springer, ISI Impact Factor (2009): 1.013