Abstract:

T-LOTOS, is a timed extension of LOTOS is described where the semantics is described in the form of timed-action trees. In timed-action trees the passing of time is represented as time stamps of actions, being each time stamp the time passed from the previous action occurred. Timed-action trees and Time/Action trees can be formally related by mapping B -at-> B´ to B -t-> B´´, B´´-a-> B´ (and viceversa). A formal framework for verifying timed systems is provided based on timed tests, by assigning a precise timing to the tests and observations performed.