From OWL-S to Timed Automata Network: Operational Semantic

In this paper we present a framework, an algorithm and a new tool for online testing of real-time systems based on symbolic techniques used in UPPAAL model checker. We extend UPPAAL timed automata network model to a test specification which is used to generate test primitives and to check the correctness of system responses including the timing aspects. We use timed trace inclusion as a conformance relation between system and specification to draw a test verdict. The test generation and execution algorithm is implemented as an extension to UPPAAL and experiments carried out to examine the correctness and performance of the tool. The experiment results are promising.

Download Full-text

C3+ATO Function Simulation and Verification Analysis Based on Timed Automata

Advances in Transdisciplinary Engineering - ISMR 2020 ◽

10.3233/atde200229 ◽

2020 ◽

Author(s):

Jie Yao ◽

Zhenhai Zhang

Keyword(s):

System Design ◽

High Speed ◽

Timed Automata ◽

Functional Requirements ◽

System Specification ◽

System Safety ◽

Verification Method ◽

Message Sequence Charts ◽

Train Operation ◽

Automata Network

C3+ATO system plays an important role in controlling train operation and its function is related to the safety of train automatic operation. A simulation and verification method based on timed automata is proposed to verify the function of high-speed railway C3+ATO system. The functional requirements in the C3+ATO system specification are extracted and the timed automata models are established and then the timed automata network model is formed. The message sequence charts are generated and system safety, reachability, existence are verified. As a result, the models meet the functional requirements of the system which provide theoretical reference for the subsequent C3+ATO system design and development, test and measurement, practical application and related specification improvement.

Download Full-text

Modeling and Verification of ARINC 653 Hierarchical Preemptive Scheduling

The International Arab Journal of Information Technology ◽

10.34028/iajit/17/1/12 ◽

2019 ◽

Vol 17 (1) ◽

pp. 99-106 ◽

Cited By ~ 1

Author(s):

Ning Fu ◽

Lijun Shan ◽

Chenglie Du ◽

Zhiqiang Liu ◽

Han Peng

Keyword(s):

Model Checking ◽

Timed Automata ◽

Automata Theory ◽

Traditional Scheduling ◽

Preemptive Scheduling ◽

Scheduling System ◽

Software Interface ◽

Precise Analysis ◽

Stop Watch ◽

Automata Network

Avionics Application Standard Software Interface (ARINC 653) is a software specification for space and time partitioning in safety-critical avionics real-time operating systems. Correctly designed task schedulers are crucial for ARINC 653 running systems. This paper proposes a model-checking-based method for analyzing and verifying ARINC 653 scheduling model. Based on priced timed automata theory, an ARINC 653 scheduling system was modeled as a priced timed automata network. The schedulability of the system was described as a set of temporal logic expressions, and was analyzed and verified by a model checker. Our research shows that it is feasible to use model checking to analyze task schedulability in an ARINC 653 hierarchical scheduling system. The method discussed modeled preemptive scheduling by using the stop/watch features of priced timed automata. Unlike traditional scheduling analysis techniques, the proposed approach uses an exhaustive method to automate analysis of the schedulability of a system, resulting in a more precise analysis

Download Full-text

Practical Approach in Verification of Security Systems Using Satisfiability Modulo Theories

Logic Journal of IGPL ◽

10.1093/jigpal/jzaa062 ◽

2020 ◽

Author(s):

Agnieszka M Zbrzezny ◽

Sabina Szymoniak ◽

Miroslaw Kurkowski

Keyword(s):

Timed Automata ◽

Security Protocols ◽

Satisfiability Modulo Theories ◽

New Method ◽

Security Systems ◽

Smt Solver ◽

Novel Method ◽

Important Time ◽

Reachability Property ◽

Automata Network

Abstract The paper presents a novel method for the verification of security protocols’ (SPs)time properties. The new method uses a translation to satisfiability modulo theories (SMT) problem. In our approach, we model protocol users’ behaviours using networks of synchronized timed automata. Suitably specified correctness properties are defined as a reachability property of some chosen states in an automata network. Then, the network of timed automata and the property are translated to an SMT problem and checked using an SMT-solver and a BMC algorithm. We consider the most important time properties of protocol executions using specially constructed time conditions. The new method was also implemented and experimentally evaluated for six well-known SPs. We also compared our new SMT-based technique with the corresponding SAT-based approach.

Download Full-text

A novel cryptosystem based on abstract automata and Latin cubes

Studia Scientiarum Mathematicarum Hungarica ◽

10.1556/012.2015.52.2.1309 ◽

2015 ◽

Vol 52 (2) ◽

pp. 221-232

Author(s):

Pál Dömösi ◽

Géza Horváth

Keyword(s):

Block Cipher ◽

Finite Automata ◽

Theoretical Background ◽

Point Of View ◽

Theoretical Point ◽

Transition Matrices ◽

Encryption And Decryption ◽

Secret Keys ◽

Automata Network ◽

Fully Functioning

In this paper we introduce a novel block cipher based on the composition of abstract finite automata and Latin cubes. For information encryption and decryption the apparatus uses the same secret keys, which consist of key-automata based on composition of abstract finite automata such that the transition matrices of the component automata form Latin cubes. The aim of the paper is to show the essence of our algorithms not only for specialists working in compositions of abstract automata but also for all researchers interested in cryptosystems. Therefore, automata theoretical background of our results is not emphasized. The introduced cryptosystem is important also from a theoretical point of view, because it is the first fully functioning block cipher based on automata network.

Download Full-text