• DocumentCode
    2973866
  • Title

    Prism2Promela

  • Author

    Power, Christopher ; Miller, Alice

  • Author_Institution
    Dept. of Comput. Sci., Univ. of Glasgow, Glasgow
  • fYear
    2008
  • fDate
    14-17 Sept. 2008
  • Firstpage
    79
  • Lastpage
    80
  • Abstract
    The Prism model checker facilitates the formal modelling and analysis of systems that exhibit random or probabilistic behaviour. Prism lacks the provision of methods for specification debugging. To help alleviate this problem, we present a tool Prism2Promela for translating Prism into Promela. Once in this form, the SPIN model checker can be used to identify errors in the Promela specification, which can be traced back to corresponding errors in the original Prism specification.
  • Keywords
    probability; program debugging; program verification; Prism model checker; Prism2Promela; Promela specification; Spin model checker; formal modelling; probabilistic behaviour; specification debugging; Context modeling; Debugging; Error correction; Formal verification; Mirrors; Power system modeling; Stochastic systems; System recovery; Prism; Spin; Verification; model checking;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Quantitative Evaluation of Systems, 2008. QEST '08. Fifth International Conference on
  • Conference_Location
    St. Malo
  • Print_ISBN
    978-0-7695-3360-5
  • Type

    conf

  • DOI
    10.1109/QEST.2008.20
  • Filename
    4634957
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=2973866