• DocumentCode
    1573051
  • Title

    Abstract model checking and refinement of temporal logic in αSPIN

  • Author

    Gallardo, Maria Del Mar ; Martínez, Jesus ; Merino, Pedro ; Pimentel, Ernesto

  • Author_Institution
    Comput. Sci. Dept., Malaga Univ., Spain
  • fYear
    2003
  • Firstpage
    245
  • Lastpage
    246
  • Abstract
    We give an overview of the features offered by the tool αSPIN in order to perform abstract model checking of LTL formulas. Shortly, these features are: construction of over-approximated PROMELA models, checking satisfaction of universal formulas, checking refutation of existential formulas, and on-the-fly refinement of the model by means of a refinement of the temporal formula to be verified.
  • Keywords
    formal verification; refinement calculus; temporal logic; αSPIN; LTL formula; PROMELA model; abstract model checking; on-the-fly refinement; temporal logic; Automata; Chromium; Concrete; Explosions; Logic;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Application of Concurrency to System Design, 2003. Proceedings. Third International Conference on
  • Print_ISBN
    0-7695-1887-7
  • Type

    conf

  • DOI
    10.1109/CSD.2003.1207725
  • Filename
    1207725
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1573051