Design and model checking of timed automata oriented architecture for Internet of thing

The architecture model of the Internet of thing system is the primary foundation for the design and implementation of the Internet of thing system. This article discusses the method and practice of time automaton modeling and model checking for the architecture of the Internet of thing system from the state and time dimensions. This article introduces the theory and method of modeling using time automata. And then, combined with the actual need of the elderly health cabin Internet of thing system, a dynamic and fault-tolerant time automaton model is established through a relatively complete architecture modeling. The model checking method verifies that the designed Internet of thing system has no deadlock system activity, service correctness, and timeliness correctness. The results of modeling experiments and model validation show that the reference model of time automata Internet of thing architecture established in this article can better reflect the nature of interaction with the physical world, heterogeneity and large-scale, dynamic, and incompleteness of the Internet of thing system.

Phase Transition in Elementary Cellular Automata with Memory

We study elementary cellular automata with memory. The memory is a weighted function averaged over cell states in a time interval, with a varying factor which determines how strongly a cell's previous states contribute to the cell's present state. We classify selected cell-state transition functions based on Lempel–Ziv compressibility of space-time automaton configurations generated by these functions and the spectral analysis of their transitory behavior. We focus on rules 18, 22, and 54 because they exhibit the most intriguing behavior, including computational universality. We show that a complex behavior is observed near the nonmonotonous transition to null behavior (rules 18 and 54) or during the monotonic transition from chaotic to periodic behavior (rule 22).

A Study on Network Protocol Validation Based on Timed Automata

With the increasingly complex of computer software system, traditional software engineering methods for major software development will inevitably produce a lot of mistakes and catastrophic consequences for key industry users. Experiment with software engineering methods cannot guarantee the behavior at infinity reliability and security of the state space. All this requires formal analysis and verification to the complex system. In protocol verification based on automatic machines, the automaton is used to represent the behavior of the system, the time automaton is a formal method can be well applied to the network protocol verification.