TriCera Web Interface

TriCera accepts programs in a C-like language, including the keywords:

• assert(condition): verify that a condition holds at this point in the program.
• assume(condition): assume that a condition holds.
• atomic { stm1; stm2; ... }: execute a block of statements atomically. atomic { assume(!lock); lock=1; } will atomically check that lock has value 0, and then set the variable to 1.
• within (cond) { stm1; stm2; ... }: execute a block of statements (atomically) before cond expires. This corresponds to time invariants in Uppaal timed automata.
• thread <name> { ... }: statically declare a (singleton) thread.
• thread[<id-var>] <name> { ... }: statically declare an infinitely replicated thread.
• clock <name>, duration <name>: declare clocks or variables representing time periods.
• chan <name>: declare a binary (UPPAAL-style) communication channel, which can be used via chan_send and chan_receive.

For more information, see our Github page.