A Formal Method for Specifying The Interface of Components in Real-time Concurrent Systems

  • Do Van Chieu

Abstract

In  this  paper,  we  propose  a  method  for specifying  the  interface  of  components  in  real-time concurrent  systems.  The  key  idea  of  the  proposed method  is  to  extend  Interface-based  design  with  using timed  trace  theory.  We  propose  a  technique  to  specify the interaction protocols of component interfaces by the languages  of  timed  words  augmented  with  the concurrency, i.e. timed trace languages. In addition, we propose a class of automata that can recognize a class of timed trace languages called timed concurrent interface automata.  We  give  an  algorithm  for  the  refinement, component  composition,  and  show  that  our  method possesses two  important  features  of  interface  automata theory  which  are  incremental  design  and  independent implementation.  Those  results  play  a  key  role  in  the specification  and  verification  of  real-time  concurrent systems
Published
2015-10-28
Section
Regular Articles