Rules for Verification of Interactive Systems

Marcelo de Almeida Maia e Roberto da Silva Bigonha

Recently, we have proposed an interaction based extention[4] to the formal method ASM[2]. The extension provides mechanisms to specify directly how pieces of specification can interact with each other. The goals of the extension are manifold, ranging, for example, from the modularization of a specification to the specification of mobile objects. In this work, we propose a type discipline for the Interactive ASMs focused on the interactive portion of the specification.