SDL-News: Assert and Progress in Tau 4.4

Subject: SDL-News: Assert and Progress in Tau 4.4
From: Cris Fuhrman (christopher.fuhrman#etsmtl.ca)
Date: Mon Mar 01 2004 - 23:55:02 GMT

• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
• Next message: Andreas Metzger: "Re: FW: SDL-News: Timers"
• Previous message: Anthony Weber: "FW: SDL-News: Timers"
• Next in thread: Cris Fuhrman: "RE: SDL-News: Assert and Progress in Tau 4.4"

Hello,

This is a question specific to Telelogic Tau 4.4, which is what we use
currently in our courses at the ETS.

Reading the documentation, I’ve come to the conclusion that it is not
possible to use the functionality of “assert” (safety property) and
“progress” (liveness property) for validation (state exploration) without
declaring the functions in C. This seems counter intuitive, since decisions
blocks (which are Booleans after all) are supported in Tau 4.4 without
having to generate C functions.

Is there a way to do xAssert/xProgress in a pure SDL model without having to
pass into the realm of C? For the early stages of my course, I would like
for my students to not be bogged down with .h files for their lightweight
models, yet still be able to validate them.

Has anyone considered SDL support for assert/progress on a higher level?

Thanks in advance,

Cris Fuhrman

--
Prof. Christopher Fuhrman
École de technologie supérieure (ETS)
P>+1 (514) 396 8638