Links to papers relevant to SAL

From SRI SAL

Timed Systems in SAL

Bruno Dutertre and Maria Sorea introduced a method for specifying and analyzing timed systems using the infinite bounded model checker of SAL. The technique uses timeout automata or their more complex variant (that includes events) called calendar automata.

B. Dutertre and M. Sorea, Timed Systems in SAL, Technical Report SRI-SDL-04-03, July 2004. pdf gzipped postscript

B. Dutertre and M. Sorea, Modeling and Verification of a Fault-Tolerant Real-Time Startup Protocol using Calendar Automata, presented at FORMATS/FTRTFT'04, LNCS 3253, pp. 119--214, Grenoble, France, September 2004. pdf gzipped postscript

Lee Pike introduced some optimizations and, with Geoffrey Brown, demonstrated application of the method to some timed protocols previously considered to pose formidable challenges to formal verification.

Lee Pike, Real-time system verification by k-induction. NASA Technical Memorandum TM-2005-213751, 2005. more info

Geoffrey Brown and Lee Pike, Easy parameterized verification of biphase and 8N1 protocols. In 12th International Conference on Tools and Algorithms for the Construction and Analysis of Algorithms (TACAS'06), volume 3920 of LNCS, pages 58--72, 2006. Springer. more info

Geoffrey M. Brown, Verification of a Data Synchronization Circuit For All Time, Sixth International Conference on Application of Concurrency to System Design (ACSD'06), pp. 217-228, IEEE Computer Society, 2006 IEEE CS digital library, IEEE Xplore

Geoffrey Brown and Lee Pike, Temporal refinement using SMT and model checking with an application to physical-layer protocols. ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'2007), 2007 more info

Mark Lawford and colleagues have used PVS and SAL to analyze Time Transition Models

Mark Lawford, Vera Pantelic, and Hong Zhang, Towards Integrated Verification of Timed Transition Models, Fundamenta Informaticae, Volume 70, Number 1-2 / 2006, Pages 75 - 110. IOS Press More info

These authors conclude "the current implementation in the general purpose SAL model-checker lags well behind state of the art real-time model-checkers". We think this conclusion is incorrect and a consequence of their very indirect encoding of the problem in SAL (as opposed to their direct encoding in UPPALL). The following tutorial presents a direct encoding of their example in SAL (using Timeout Automata) and executes in milliseconds.

Bruno Dutertre, Model Checking Infinite-state Systems in SAL, from AFM 2006 (a workshop at CAV 2006, Seattle WA). pdf SAL files

[edit]

Interrupt-Driven Software

Colin Fidge, Phil Cook, "Model Checking Interrupt-Dependent Software," 12th Asia-Pacific Software Engineering Conference (APSEC'05), 2005, pp. 51--58. pdf

[edit]