عنوان فارسی کارگاه:بررسی مدل و اثبات ویژگیهای رفتاری سیستمها
عنوان انگلیسی کارگاه: Model Checking and Verification of Behavioral Properties of Systems
ارائه کننده: سعید پاشازاده –دانشیار دانشکده مهندسی برق و کامپیوتر دانشگاه تبریز
روشهای رسمی مبتنی بر ریاضیات هستند و با هدف قابلیت اثبات ویژگیهای رفتاری سیستمهای مختلف ایجاد شدهاند. زبانهای رسمی مختلفی وجود دارند که هر کدام از آنها برای اثبات برخی ویژگیهای محدود و یا سیستمهای خاصی ایجاد شدهاند. اغلب روشهای رسمی قابلیت تعمیم پایینی برای استفاده در حوزههای متنوع دارند. شبکه پتری رنگی سلسله مراتبی توسعهای از شبکه پتری سنتی است که قابلیت مدلسازی آن بهطرز چشمگیری توسعه یافته است. این روش رسمی برای مدلسازی و بررسی ویژگیهای رفتاری سیستمهای همروند در مرحله طراحی ابداع شده است. شبکه پتری رنگی دارای واسط گرافیکی ساده بوده و از زبان هوش مصنوعی ML استفاده میکند و مبتنی بر تئوری کیسه است و یکی از روشهای رسمی پرکاربرد محسوب میشود که قابلیت بسیار زیادی در مدل سازی انواع سیستمهای توزیعی و همروند دارد. در شبکه پتری رنگی، مدل ایجاد شده برای اثبات ویژگیهای رفتاری سیستم با انجام تغییرات جزئی، قابلیت استفاده برای شبیهسازی و استخراج معیارهای کارآیی سیستم را هم دارد. بدین ترتیب با ایجاد یک مدل، ابتدا صحت ویژگیهای رفتاری سیستم اثبات شده و سپس معیارهای کمی کارآیی سیستم با همان مدل قابل استخراج است.
در این کارگاه مد نظر است که ابتدا شبکه پتری کلاسیک و مبنای ریاضی آن بطور اجمالی معرفی شود. سپس شبکه پتری رنگی معرفی خواهد شد و بطور اجمالی زبان هوش مصنوعی ML معرفی خواهد شد. در ادامه یک سیستم نمونه با استفاده از ابزار متن باز CPN Tools با شبکه پتری رنگی سلسله مراتبی مدلسازی و اجرا شده و فضای حالت آن استخراج خواهد شد. سپس بررسی مدل به همراه زبانهای LTL و CTLمعرفی خواهند شد و چند ویژگی رفتاری پر کاربرد با این زبانها فرموله خواهند شد. سپس این ویژگیها با جستجو در گراف فضای حالت اثبات خواهند شد. در انتها نحوه شبیهسازی سیستم با استفاده از مدل توسعه یافته و استخراج معیارهای کارآیی سیستم نمایش داده خواهد شد.
JOURNAL PAPERS
- S. Najjar Ghabel,S. Pashazadeh,”Modeling Automatic Generator of Optimal and Minimal Covers of Functional Dependency”,Indian Journal of Science and Technology,Vol. 8,no. 35,December 2015.
- S. Pashazadeh,M. Rahimi,”Modeling Timestamp Ordering Method Using Colored Petri Net”,Indian Journal of Science and Technology,Vol. 8,no. 35,December 2015.
-
S. Pashazadeh,”Automatic Analysis of Computer Game Using Colored Petri Net”,Tabriz
Journal of Electrical Eng. (Accepted).
- S. Pashazadeh,S. Saeedvand,”Modelling of Walking Humanoid Robot with Capability of Floor Detection and Dynamic Balancing Using Colored Petri Net”,International Journal in Foundations of Computer Science & Technology (IJFCST),Vol. 4,No. 2,pp. 1-10,March 2014.
- S. Pashazadeh,E. Abdolrahimi Niyari,”Modeling Enterprise Architecture Using Timed Colored Petri Net: Single Processor Scheduling”,International Journal of Managing Public Sector Information and Communication Technologies (IJMPICT),Vol. 5,No. 1,pp. 1-13,March 2014.
- A. Keshvari Ilkhichi,S. Pashazadeh,“Modelling Kerberos Authentication Protocol Using Colored Petri Net”,International Journal of Information & Network Security (IJINS),Vol. 2,No. 5,pp. 403-416,October 2013.
- S. Pashazadeh,”Modeling and Verification of Deadlock Potentials of a Concurrency Control Mechanism in Distributed Databases Using Hierarchical Colored Petri Net”,International Journal of Information and Education Technology (IJIET),Vol. 2,No. 2,April 2012,pp.77-82.
- S. Tafkiki Alamdari,S. Pashazadeh,and H. Mirzamohammadzadeh,”Security Analysis of CARBAC Model in Pervasive Computing Environment Using Colored Petri Net”,Journal of Computing,Vol. 4,No. 7,July 2012,pp. 61-69.
- S. Pashazadeh and M. Pashazadeh,”Modeling an Automatic Proof Generator for Functional Dependency Rules Using Colored Petri Net”,International Journal in Foundations of Computer Science & Technology (IJFCST),Vol. 2,No. 5,September 2012,pp. 31-47.
- S. Pashazadeh,”Modeling and Verification of Access Rights in Take-Grant Protection Model Using Colored Petri Nets” International Journal of Information & Network Security (IJINS),Vol. 2,No. 1,February 2013,pp. 413-425.
NATIONAL & INTERNATIONAL CONFERENCE PAPERS
- E.V. Arekhloo,S. Pashazadeh,S.N. Razavi,”Modelling of Mamdani Fuzzy Inference Engine using hierarchical colored Petri nets”,13th Iranian Conference on Fuzzy Systems (IFSC),Qazvin,Iran,Aug. 27-29,2013.
- S. Pashazadeh,“Modeling a Concurrency Control Mechanism in Distributed Databases using Hierarchical Colored Petri Net“,2012 International Conference on Information and Computer Applications (ICICA 2012),IPCSIT vol. 24 (2012) IACSIT Press,Singapore,Hong Kong,China,February 17-18,2012,pp. 286-289.
- S. Pashazadeh,“Modeling a Resource Management Method Using Hierarchical Colored Petri Nets”,International eConference on Computer and Knowledge Engineering (ICCKE2011),Mashhad,Iran,October 13-14,2011,pp. 55-60.