An efficient model checker based on theaxiomatization of Propositional Temporal Logic in rewriting logic
Author | Rebaiaia, M.L. |
Author | Jaam, J.M. |
Author | Hasnah, A.M. |
Available date | 2024-03-20T01:55:09Z |
Publication Date | 2003 |
Publication Name | Proceedings of the IEEE International Conference on Electronics, Circuits, and Systems |
Resource | Scopus |
Abstract | In this paper, we propose an efficient Model Checker for the Propositional Temporal Logic denoted by PTL. This logic is hown to be well suited to verify electronic circuits and reactive systems. A typical verification problem consists of establishing formally a relatiombip between the specification of a software/hardware system and its implementation. In the sequel we show how a bardware designer should proceed to specify his design and prove its correctness using a PTL module under Maude System. A series of experiments have been conducted successfully on a well-known benchmark to prove the effectiveness of mixing temporal logic and rewriting logic techniques. |
Language | en |
Publisher | IEEE |
Subject | Computer science Logic circuits Computer crashes Boolean functions Equations Electronic circuits Computer bugs Modems Humans Rockets |
Type | Conference |
Pagination | 866-869 |
Volume Number | 2 |
Files in this item
Files | Size | Format | View |
---|---|---|---|
There are no files associated with this item. |
This item appears in the following Collection(s)
-
Computer Science & Engineering [2402 items ]