Links to papers relevant to SAL

Jump to: navigation, search


Network Models and Analyses

Douglas Browne, Formal network behaviour analysis using model checking. Masters by Research thesis, Queensland University of Technology, 2016.

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


TTEthernet is a communication infrastructure for mixed-criticality systems that integrates dataflow from applications with different criticality levels on the same network. For applications of highest criticality TTEthernet provides a synchronization strategy that tolerates multiple failures. Several aspects of this synchronization strategy have been analysed using SAL.

  • Wilfried Steiner and Bruno Dutertre, SMT-Based Formal Verification of TTEthernet Synchronization Functions (Models and Proofs), The Permanence Function builds an algorithmic interface between network jitter imposed by the dataflow-integration and the actual synchronization strategy. The Compression Function is a core element of the TTEthernet clock synchronization service.
  • Wilfried Steiner and Bruno Dutertre, Automated Formal Verification of the TTEthernet Synchronization Quality (Extended Version), This paper describes how the SAL model checker sal-inf-bmc has been applied to formally prove the precision in a TTEthernet network. The paper will be presented at the third NASA Formal Methods Symposium in April 2011 and the extended version will be uploaded afterwards. The models can be downloaded here.

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

Z and SAL

  • John Derrick, Siobhán North, and Tony Simons, Issues in Implementing a Model Checker for Z, ICFEM 2006, LNCS 4260, pp. 678--696. LNCS
  • Graeme Smith and Luke Wildman, Model Checking Z Specifications Using SAL, ZB 2005, LNCS 3455, pp. 85--103 LNCS
Personal tools