Computer Engineering / Bilgisayar Mühendisliği
Permanent URI for this collectionhttps://hdl.handle.net/11147/10
Browse
3 results
Search Results
Conference Object Citation - Scopus: 7Utilization of Timed Automata as a Verification Tool for Security Protocols(Institute of Electrical and Electronics Engineers Inc., 2010) Koltuksuz, Ahmet; Külahçıoğlu, Burcu; Özkan, MuratTimed Automata is an extension to the automata-theoretic approach for the modeling of real time systems that introduces time into the classical automata. It has become an important research area in both the context of formal languages and modeling and verification of real time systems since it was proposed by Alur and Dill in the early nineties. Timed automata proposes an efficient model checking method for verification real time systems having mature and efficient automatic verification tools. One of the application areas of timed automata is the verification of security protocols which are known to be time sensitive. This study aims to make use of timed automata as a verification tool for security protocols and gives a case study on the initial part of the Neuman- Stubblebine Repeated Authentication Protocol. © 2010 IEEE.Conference Object Citation - Scopus: 2Towards Test Case Generation for Synthesizable Vhdl Programs Using Model Checker(Institute of Electrical and Electronics Engineers Inc., 2010) Ayav, Tolga; Tuğlular, Tuğkan; Belli, FevziVHDL programs are often tested by means of simulations, relying on test benches written intuitively. In this paper, we propose a formal approach to construct test benches from system specification. To consider the real-time properties of VHDL programs, we first transform them to timed automata and then perform model checking against the properties designated from the specification. Counterexamples returned from the model checker serve as a basis of test cases, i.e. they are used to form a test bench. The approach is demonstrated and complemented by a simple case study.Conference Object Model Based Testing of Vhdl Programs(Institute of Electrical and Electronics Engineers Inc., 2015) Ayav, Tolga; Tuğlular, Tuğkan; Belli, FevziVHDL programs are often validated by means of test benches constructed from formal system specification. To include real-time properties of VHDL programs, the proposed approach first transforms them to concurrently running network of timed automata and then performs model checking on properties taken from the specification. Counterexamples generated by the model checker are used to form a test bench. The approach is validated by a case study composed of a nontrivial application running on a microprocessor. As presented, the approach enables testing both hardware and software at once.