Free Trial

Safari Books Online is a digital library providing on-demand subscription access to thousands of learning resources.

  • Create BookmarkCreate Bookmark
  • Create Note or TagCreate Note or Tag
  • PrintPrint

CONCLUSION

Timed automata is an established and widely used formalism that has proven very useful for specifying and formally verifying distributed embedded systems. However, the fact that all the clocks of a timed automaton must evolve at the same rate is often considered as a shortcoming for realistic modeling of distributed systems, since clocks with variable rate cannot be directly modeled. Fortunately, a number of modeling techniques exist that allow system developers to circumvent this limitation and specify clocks of variable rate. This chapter has been devoted to presenting and discussing these techniques in a systematic way.

Furthermore, and prior to the description of these techniques, a taxonomy of the types of clocks that may be found in a distributed embedded system has been presented. This taxonomy is useful for modeling distributed embedded systems because it allows system developers to fully understand the implicit assumptions of the computer clocks they use. As we have indicated, the fact that clock synchronization is a transparent service sometimes makes the system developers not really aware of certain subtleties that are important for the correct modeling of the system.


  

You are currently reading a PREVIEW of this book.

                                                                                                                    

Get instant access to over $1 million worth of books and videos.

  

Start a Free Trial


  
  • Safari Books Online
  • Create BookmarkCreate Bookmark
  • Create Note or TagCreate Note or Tag
  • PrintPrint