Home| Contact Us| New Journals| Browse Journals| Journal Prices| For Authors|

Print ISSN: 0976-3503
Online ISSN:
0976-2930


  About JET
  DLINE Portal Home
Home
Aims & Scope
Editorial Board
Current Issue
Next Issue
Previous Issue
Sample Issue
Upcoming Conferences
Self-archiving policy
Alert Services
Be a Reviewer
Publisher
Paper Submission
Subscription
Contact us
 
  How To Order
  Order Online
Price Information
Request for Complimentary
Print Copy
 
  For Authors
  Guidelines for Contributors
Online Submission
Call for Papers
Author Rights
 
 
RELATED JOURNALS
Journal of Digital Information Management (JDIM)
International Journal of Computational Linguistics Research (IJCL)
International Journal of Web Application (IJWA)

 

 
Journal of E-Technology

The Application of SMT Solvers in the Mission Critical Software Verification
Andrey Tyugashev, Dmitrii Zheleznov
Samara State Transport University, 2V Svobody Street, Samara 443066 & Russia
Abstract: We have discussed the application of SMT solvers in the Mission Critical Software verification. We have developed the Rules of verification based on Real-Time Control Algorithm’s Logic. Required specification can be feasible or non-feasible on defined basis of functional control processes. In this model, the feasibility of the specification is being checked by SMT solver Z3. We have used a particular Java application through API for the SMT solver.
Keywords: Control Logic, Functional Process, Logical Vector, Real-time Control Algorithm, Logic Programming, SMT Solver The Application of SMT Solvers in the Mission Critical Software Verification
DOI:https://doi.org/10.6025/jet/2021/12/3/86-92
Full_Text   PDF 546 KB   Download:   217  times
References:

[1] Ashby, W. (1956). Introduction to Cybernetics, – New York, Chapman & Hall.
[2] Akhmetov, R. N., Makarov, V. P., Sollogub, A. V. (2012). Principles of the Earth Observation Satellites Control in Contingencies, Information and Control Systems, vol. 1, p. 16-22.
[3] Tyugashev, A. A. (2006). Integrated environment for designing realtime control algorithms, Journal of Computer and Systems Sciences International, 2 (45) 287-300.
[4] Kalentyev, A. A., Tiugashev, A. A. (2006). Application of CALS technologies in Lifecycle of Complex Control Software, Samara, Samara Centre of RAS Publishing, (in Russian).
[5] Tyugashev, A., Ilyin, I., Ermakov, I. (2012). Ways to improve quality and reliability of software in aerospace industry, Large-Scale Systems Control, p. 288–299, vol. 39, (in Russian).
[6] Tyugashev, A. (2017). Use of graph-based and algebraic models in lifecycle of real-time flight control software, In: Proceedings of Mathematical Modeling Session at the International Conference Information Technology and Nanotechnology (MM-ITNT 2017) p. 306-311, Samara, Russia, 19.11.2017.
[7] Tiugashev, A. (2017). Build and evaluation of real-time control algorithms in case of incomplete information about functional processes’ parameters, In: Proceedings of 2017 XX IEEE International Conference on Soft Computing and Measurements (SCM’2017), p. 179-185, Saint Petersburg, Russia.


Home | Aim & Scope | Editorial Board | Author Guidelines | Publisher | Subscription | Previous Issue | Contact Us |Upcoming Conferences|Sample Issues|Library Recommendation Form|

 

Copyright © 2011 dline.info