IDEAS home Printed from https://ideas.repec.org/a/igg/jncr00/v2y2011i3p1-12.html
   My bibliography  Save this article

Towards Automated Verification of P Systems Using Spin

Author

Listed:
  • Raluca Lefticaru

    (University of Pitesti, Romania)

  • Cristina Tudose

    (University of Pitesti, Romania)

  • Florentin Ipate

    (University of Pitesti, Romania)

Abstract

This paper presents an approach to P systems verification using the Spin model checker. The authors have developed a tool which implements the proposed approach and can automatically transform P system specifications from P-Lingua into Promela, the language accepted by the well known model checker Spin. The properties expected for the P system are specified using some patterns, representing high level descriptions of frequently asked questions, formulated in natural language. These properties are automatically translated into LTL specifications for the Promela model and the Spin model checker is run against them. In case a counterexample is received, the Spin trace is decoded and expressed as a P system computation. The tool has been tested on a number of examples and the results obtained are presented in the paper.

Suggested Citation

  • Raluca Lefticaru & Cristina Tudose & Florentin Ipate, 2011. "Towards Automated Verification of P Systems Using Spin," International Journal of Natural Computing Research (IJNCR), IGI Global, vol. 2(3), pages 1-12, July.
    • Handle: RePEc:igg:jncr00:v:2:y:2011:i:3:p:1-12
    as

    Download full text from publisher

    File URL: http://services.igi-global.com/resolvedoi/resolve.aspx?doi=10.4018/jncr.2011070101
    Download Restriction: no
    ---><---

    More about this item

    Statistics

    Access and download statistics

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:igg:jncr00:v:2:y:2011:i:3:p:1-12. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    We have no bibliographic references for this item. You can help adding them by using this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: Journal Editor (email available below). General contact details of provider: https://www.igi-global.com .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.