Font Size: a A A

Finite Quantified Linear Temporal Logic And Its Satisfiability Checking

Posted on:2024-04-08Degree:MasterType:Thesis
Country:ChinaCandidate:Y ChenFull Text:PDF
GTID:2568307067493274Subject:Software engineering
Abstract/Summary:PDF Full Text Request
In this paper,we present Finite Quantified Linear Temporal Logic(FQLTL),a new formal specification language that extends Linear Temporal Logic(LTL)with quantifiers over finite domains.Explicitly,FQLTL leverages quantifiers and predicates to constrain the domains in the system and utilizes temporal operators from LTL to specify properties with time sequences.Compared to LTL,FQLTL is more suitable and accessible to describe the specification with both restricted domains and temporal properties,which can be applied to the scenarios such as railway transition systems.In addition,this paper proposes a methodology to check FQLTL satisfiability,releasing the corresponding checker for potential users to further use.Applying formal methods to large,security-critical systems is highly recommended and makes sense.Based on the proposed new language FQLTL,its definition and relevant theory,the paper illustrates the applicability of the language and its value to specific industries with sufficient cases and implementable experiments.This paper is based on a project with rail interlocking system as a background.We give in detail the process from the proposed language to the implementation of satisfiability checking and the corresponding algorithmic architecture.Towards experiments,we show that by applying the logic to the railway transit system,most of the safety specifications can be formalized and several inconsistent specifications are reported through our implemented satisfiability checker.
Keywords/Search Tags:formal method, linear temporal logic, formal language, interlocking system
PDF Full Text Request
Related items