Automated proof for equivalence of telephone systems
| Autor: | Noriaki Yoshimasa, Yoshinobu Kawabe, Jun Sakoh |
|---|---|
| Rok vydání: | 2013 |
| Předmět: |
Physics::Physics and Society
Theoretical computer science Computer science business.industry Computability Computer Science::Computation and Language (Computational Linguistics and Natural Language and Speech Processing) Computer Science::Human-Computer Interaction Computer Science::Computers and Society Alloy Analyzer Formal specification Telephony Equivalence (formal languages) business Formal verification |
| Zdroj: | ICIS |
| DOI: | 10.1109/icis.2013.6607888 |
| Popis: | An extended telephone system to avoid a phone fraud was introduced by Yamamoto et al. In this study, we prove that the extended telephone system is equivalent to the original telephone system at a level of abstraction. We conduct an automatic proof with the Alloy analyzer. After describing specifications of telephone systems in I/O-automaton, we translate the specifications into Alloy. We finally prove the existence of forward simulations by SAT solving. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|