Model checking embedded and real time systems
Kim G. Larsen · 2008
Given that the 2007 Turing Award was recently given to Ed Clarke, Alan Emerson and Joseph Sifakis for their ground-breaking work on model checking the talk will present two model checking tools, UPPAAL and visualSTATE. The ldquosecretsrdquo behind their success will be revealed, UPPAAL being the most efficient tool for verifying timed systems, and visualSTATE allowing for verification of 10500states using a patented method we have developed. Also, current research on applying and specializing UPPAAL to controller synthesis will be addressed.