Survey Metode Formal dalam Verifikasi dan Validasi
DOI:
https://doi.org/10.30595/juita.v4i1.1181Keywords:
Metode Formal, Verifikasi dan Validasi, SurveyAbstract
Paper ini ditujukan untuk mensurvey metode formal yang digunakan orang baik itu dalam usaha mengembangkan software & harware, atau dalam usaha melakukan verifikasi dan validasi. Beberapa metode formal yang hendak ditinjau adalah CPN, PFSA, Actor Model, Rebeca, LTL, ACTL, CTL, UML, Hybrid Automata dan ASM. Pada setiap tinjauan, dijelaskan motivasi dan gagasan dasar metode formal bersangkutan secara intuitif dan implementasi-implementasinya yang merujuk pada berbagai paper-paper penelitian yang telah dilakukan orang menyangkut metode formal bersangkutan.
References
Carl Hewitt, Hendry Baker Jr, "Actors and Continous Functionals", Massachusetts Institut of Technology, Laboratory for Computer Science, 1977, Cambridge, Massachusetts.
Christophe Scholliersa, EÌric Tanterb, Wolfgang De Meutera, "Parallel actor monitors: Disentangling task-level parallelism from data partitioning in the actor model", Science of Computer Programming, Volume 80, Part A, 1 February 2014, Pages 52-64, (ScienceDirect.com).
Joeri De Koster, Stefan Marr, Theo D'Hondt, Tom Van Cutsem, "Domains: Safe sharing among actors Original Research Article" Science of Computer Programming, In Press, Corrected Proof, Available online 18 February 2014, (ScienceDirect.com).
Hossein Hojjat, "Rebeca2 Reference Manual version 1.0.2" Formal Lab, University of Teheran, Desember 18, 2006.
Arni Hermann Reynisson, Marjan Sirjani, Luca Aceto, Matteo Cimini, Ali Jafari, Anna Ingolfsdottir, Steinar Hugi Sigurdarson, "Modelling and simulation of asynchronous real-time systems using Timed Rebeca" Original Research Article
Science of Computer Programming, Volume 89, Part A, 1 September 2014, Pages 41-68, (ScienceDirect.com).
Hamid Reza Shahriari, Mohammad Sadegh Makarem, Marjan Sirjani, Rasool Jalili, Ali Movaghar, "Vulnerability analysis of networks to detect multiphase attacks using the actor-based language Rebeca", Computers & Electrical Engineering, Volume 36, Issue 5, September 2010, Pages 874-885, (ScienceDirect.com).
J. Barnat, J. Havlicek, P. Rockai, "Distributed LTL Model Checking with Hash Compation" Electrical notes in theoritical computer science 296 (2013) 79 93 (ScienceDirect.com).
Salamah Salamah, Ann Gates, Vladick Kreinovick, "Validated Templates for Specifications of Complex LTL Formula", The Journal of Systems and Software 85 (2012) 1915-1926, (ScienceDirect.com).
N. Benes, L. Brim, B. Buhnova, I. Cerna, J. Sochor, P.Varekova, "Partial Order Reduction for State/Event LTL with Application to Component-Interaction Automata" Science of Computer Programming 76 (2011) 877-890, (ScienceDirect.com).
Sjoerd Cranen, Jan Friso Groote*, Michel Reniers "A Linier Translation from CTL* to the First Order Modal μ-calculus", Theoritical Computer Science 412 (2011) 3129 3139, (ScienceDirect.com).
Robert Meolic, Tatjana Kapus, Zmago Brezocˇnik, "CTL and ACTL patterns", EUROCON 2001, July 5-7, Bratislava, Slovak Republic.
Robert Meolic, Tatjana Kapus, Zmago Brezocˇnik, "Model Checking: A Formal Method for Safety Assurance of Logistic Systems", 2nd Congress Transport - Trafffic - Logistics, October 2-3, 2000, Portorozˇ, Slovenia.
Arjan Van der Schaft, Hans Schumacher, "An Introduction to Hybrid Dynamical Systems", Department of Systems, Signals Faculty of Mathematical Sciences
and Control University of Twente and CWI, Centre for Mathematics and Computer Science, Amsterdam and Department of Econometrics and Center for Economic Research, Tilburg University.
Zhi Han, Alongkrit Chutinan, Bruce H. Krogh, "ACTL Strong Negation and its Application to Hybrid System Verification", Control Engineering Practice 14 (2006) 1259-1267, (ScienceDirect.com).
Sinan Si Alhir, "Learning UML", Publisher O'Really, July 2003, ISBN 0-596-00344-7.
Egon Bo ̈rger, Alessandra Cavarra, Elvinia Riccobene, "On formalizing UML state machines using ASMs", Information and Software Technology 46 (2004) 287–292, http://www.sciencedirect.com.ezproxy.ugm.ac.id.
Ken Webb, Tony White, "UML as a cell and biochemistry modeling language" , BioSystems 80 (2005) 283–302, http://www.sciencedirect.com.ezproxy.ugm.ac.id.
Bogdan Aman, Gabriel Ciobanu. "Properties of enhanced mobile membranes via coloured Petri nets", Information Processing Letters 112 (2012) 243–248, http://www.sciencedirect.com.ezproxy.ugm.ac.id.
Maria Pia Fanti, Stefano Mininel, Walter Ukovich, Federica Vatta, "Modelling alarm management workflow in healthcare according to IHE framework by coloured Petri Nets", Engineering Applications of Artificial Intelligence 25 (2012) 728–733, http://www.sciencedirect.com.ezproxy.ugm.ac.id.
Yicheng Wen, Asok Ray, "Vector space formulation of probabilistic finite state automata", Journal of Computer and System Sciences 78 (2012) 1127–1141, http://www.sciencedirect.com.ezproxy.ugm.ac.id.
Kushal Mukherjee, Asok Ray, "State splitting and merging in probabilistic finite state automata for signal representation and analysis", Signal Processing 104 (2014) 105–119, http://www.sciencedirect.com.ezproxy.ugm.ac.id.
Yuri Gurevich, Margus Veanes, Charles Wallace, "Can Abstract State Machine be useful in language theory?", Theoritical Computer Science 376 (2007) 17-29, http://www.sciencedirect.com.ezproxy.ugm.ac.id.
Martin Ouimet, Kristina Lundqvist, "Automated Verification of Completness
and Consistency of Abstract State Machine Specification using a SAT Solver",
Electronic Notes Theoritical Computer Science 190 (2007) 85-97, http://www.sciencedirect.com.ezproxy.ugm.ac.id.
Miguel Carillo, David A. Rosenblueth, CTL Update of Kripke Models Througs Protections", Artificial Intelligence 211 (2014) 51-74, (ScienceDirect.com).
Downloads
How to Cite
Issue
Section
License
JUITA: Jurnal Informatika is licensed under a Creative Commons Attribution 4.0 International License.
