Refine your search
Collections
A B C D E F G H I J K L M N O P Q R S T U V W X Y Z All
Raza Kazmi, Syed Asad
- Executable Semantics for the Formal Specification and Verification of E-agents
Abstract Views :189 |
PDF Views:0
Authors
Affiliations
1 Department of Computer Science, Government College University, Lahore - 5400, PK
1 Department of Computer Science, Government College University, Lahore - 5400, PK
Source
Indian Journal of Science and Technology, Vol 8, No 16 (2015), Pagination:Abstract
Background: Software agents are expected to work autonomously and deal with unfamiliar situations astutely. Achieving cent percent test case coverage for these agents has always been a problem due to limited resources. Also a high degree of dependability is expected from autonomous software agents. Formal verification of these systems can be done by specifying the possible actions of the agents to increase the confidence in the correctness of such systems. Methods: We have used social approach of agent communication where actions of the agents are described as social obligation between the participants. Formal specification of e-agents was done using μ-calculus as it is more expressive than Linear Temporal Logic (LTL). An algorithm has been given for syntactic conversion of μ-calculus formulas to TAPA model checker environment. Results: Using converstion algorithm syntactically modified μ-calculus formulas will be executed on TAPA model checker to verify the system being modelled for the specified properties. Application: The study will help to provide future directions for formal modelling of e-agents for their correct functioning.Keywords
Agent Communication, Model Checking, μ-Calculus, μ TAPA Model Checker- Temporal Modelling and Verification of Multi-Robot Concurrent Activities
Abstract Views :159 |
PDF Views:0
Authors
Affiliations
1 Department of Computer Science, Government College University, Lahore,, PK
2 Department of Computer Science, Government College University, Lahore, PK
1 Department of Computer Science, Government College University, Lahore,, PK
2 Department of Computer Science, Government College University, Lahore, PK
Source
Indian Journal of Science and Technology, Vol 9, No 48 (2016), Pagination:Abstract
Objectives: In this work, we have introduced a method for formally verifying the concurrent activities of multiple robots. The objective is to formalize a framework for concurrent systems by using temporal logics. Methods/Statistical Analysis: The movement of the robots in given environment is modelled as a weighted transition system and the target is specified in Linear Temporal Logic (LTL) formulae over a set of propositions. Findings: The LTL formulas are characterized to handle the uncertainty or any abnormal activity during the process. The system is designed using SPIN model checker in which different LTL properties are verified. A theoretical description is supported by some experimental results, generated using the existing logics and techniques. Application/ Improvement: This work can be implemented for the surveillance task in pickup and delivery network.Keywords
Formal Verification, Model Checking, Path Planning, Robotics- Optimized Application Level Checkpoint Based Load Sharing Model for Heterogeneous Mobile Grid Computing
Abstract Views :246 |
PDF Views:0
Authors
Imran Rafique
1,
Hina Gul
2,
Salman Rafique
3,
Syed Asad Raza Kazmi
1,
Awais Qasim
1,
Ilyas Fakhir
1
Affiliations
1 Department of Computer Science, GC University, Lahore – 54000, PK
2 Department of Computer Science, Kinnaird College for Women, Lahore– 54000, PK
3 Department of Computer of Science and Engineering, University of Engineering and Technology, Lahore − 54890, PK
1 Department of Computer Science, GC University, Lahore – 54000, PK
2 Department of Computer Science, Kinnaird College for Women, Lahore– 54000, PK
3 Department of Computer of Science and Engineering, University of Engineering and Technology, Lahore − 54890, PK