Abstract:
We consider the verification problem for an electromechanical device with a variable number of connectors and solve it with the modal logic LTL (Linear Temporal Logic). In the course of the analysis, we prove continuity and unambiguity theorems for the device operation and study the restrictions necessary in order for the device operation algorithm to be completely correct.
Citation:
A. N. Nepeivoda, “Verification of a technical system model with linear temporal logic”, Avtomat. i Telemekh., 2012, no. 9, 124–140; Autom. Remote Control, 73:9 (2012), 1539–1552
\Bibitem{Nep12}
\by A.~N.~Nepeivoda
\paper Verification of a~technical system model with linear temporal logic
\jour Avtomat. i Telemekh.
\yr 2012
\issue 9
\pages 124--140
\mathnet{http://mi.mathnet.ru/at4065}
\zmath{https://zbmath.org/?q=an:1258.93019}
\transl
\jour Autom. Remote Control
\yr 2012
\vol 73
\issue 9
\pages 1539--1552
\crossref{https://doi.org/10.1134/S0005117912090081}
\isi{https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=Publons&SrcAuth=Publons_CEL&DestLinkType=FullRecord&DestApp=WOS_CPL&KeyUT=000308815500008}
\scopus{https://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-84868582174}
Linking options:
https://www.mathnet.ru/eng/at4065
https://www.mathnet.ru/eng/at/y2012/i9/p124
This publication is cited in the following 4 articles:
Hein Z., Vysochkin A.V., Htoo T.P., Kvach I A., Portnov E.M., “Research and Development of a Smart Contract Algorithm For the Implementation of Block-Chain Technology on Mobile Devices”, Proceedings of the 2021 IEEE Conference of Russian Young Researchers in Electrical and Electronic Engineering (Elconrus), IEEE Nw Russia Young Researchers in Electrical and Electronic Engineering Conference, IEEE, 2021, 2299–2303
Navimipour N.J., Navin A.H., Rahmani A.M., Hosseinzadeh M., “Behavioral Modeling and Automated Verification of a Cloud-Based Framework To Share the Knowledge and Skills of Human Resources”, Comput. Ind., 68 (2015), 65–77
Navimipour N.J., “a Formal Approach For the Specification and Verification of a Trustworthy Human Resource Discovery Mechanism in the Expert Cloud”, Expert Syst. Appl., 42:15-16 (2015), 6112–6131
Long Shigong, Yang Hanwen, “Modelling Peterson Mutual Exclusion Algorithm in Dve Language and Verifying Ltl Properties”, Applied Decisions in Area of Mechanical Engineering and Industrial Manufacturing, Applied Mechanics and Materials, 577, ed. Fan K., Trans Tech Publications Ltd, 2014, 1012–1016