A model and a toolkit for the formal specification of weakly synchronous systems

The concept of weakly synchronous systems, that is systems where task nominal durations are potentially submitted to temporal jitter, offers a generic frame that covers the whole range of systems from the fully synchronous ones (i.e. systems with no jitter) to the fully asynchronous ones (i.e. systems with unbounded jitter). This paper describes a new model called HTSPN that allows a formal, accurate and complete specification of synchronization constraints inside weakly synchronous systems to be done. Moreover in order to make easier the task of specifying with HTSPN we have developed a toolkit that allows a large set of edition, verification and simulation tasks to be automatically done