{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,12]],"date-time":"2025-10-12T02:25:36Z","timestamp":1760235936083,"version":"build-2065373602"},"reference-count":53,"publisher":"MDPI AG","issue":"10","license":[{"start":{"date-parts":[[2021,10,10]],"date-time":"2021-10-10T00:00:00Z","timestamp":1633824000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computers"],"abstract":"<jats:p>This paper describes a proposed method and technology of safety assessment of projects based on field programmable gate arrays (FPGA). Safety assessment is based on special invariants, e.g., properties which remain unchanged when a specified transformation is applied. A classification and examples of FPGA project invariants are provided. In the paper, two types of invariants are described. The first type of invariants used for such assessment are those which are versatile since they reflect the unchanged properties of FPGA projects, hardware description languages, etc. These invariants can be replenished as experience gained in project implementation accumulates. The second type of invariants is formed based on an analysis of the specifics of a particular FPGA project and reflects the features of the tasks to be solved, the algorithms that are implemented, the hardware FPGA chips used, and the computer-aided design tools, etc. The paper contains a description of the overall conception and particular stages of FPGA projects invariant-based safety assessment. As examples for solving some tasks (using of invariants and defect injections), the paper contains several algorithms written in the VHSIC hardware description language (VHDL). The paper summarizes the results obtained during several years of practical and theoretical research. It can be of practical use for engineers and researchers in the field of quality, reliability, and security of embedded systems, software and information management systems for critical and business applications.<\/jats:p>","DOI":"10.3390\/computers10100125","type":"journal-article","created":{"date-parts":[[2021,10,10]],"date-time":"2021-10-10T21:19:32Z","timestamp":1633900772000},"page":"125","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Invariant-Based Safety Assessment of FPGA Projects: Conception and Technique"],"prefix":"10.3390","volume":"10","author":[{"given":"Vyacheslav","family":"Kharchenko","sequence":"first","affiliation":[{"name":"Department of Computer Systems, Networks and Cybersecurity, National Aerospace University \u201cKhAI\u201d, 17, Chkalov str., 61070 Kharkiv, Ukraine"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4672-6400","authenticated-orcid":false,"given":"Oleg","family":"Illiashenko","sequence":"additional","affiliation":[{"name":"Department of Computer Systems, Networks and Cybersecurity, National Aerospace University \u201cKhAI\u201d, 17, Chkalov str., 61070 Kharkiv, Ukraine"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5425-4098","authenticated-orcid":false,"given":"Vladimir","family":"Sklyar","sequence":"additional","affiliation":[{"name":"Department of Computer Systems, Networks and Cybersecurity, National Aerospace University \u201cKhAI\u201d, 17, Chkalov str., 61070 Kharkiv, Ukraine"}]}],"member":"1968","published-online":{"date-parts":[[2021,10,10]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","unstructured":"Grimm, T., Lettnin, D., and H\u00fcbner, M. (2018). A Survey on Formal Verification Techniques for Safety-Critical Systems-on-Chip. Electronics, 7.","DOI":"10.3390\/electronics7060081"},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Yasko, A., Babeshko, E., and Kharchenko, V. (2017, January 2\u20136). Verification of FPGA Based NPP I&C Systems Considering Multiple Faults: Technique and Automation Tool. Proceedings of the 25th International Conference on Nuclear Engineering, Shanghai, China.","DOI":"10.1115\/ICONE25-67065"},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/s11390-015-1530-5","article-title":"SRAM-based FPGA systems for safety-critical applications: A survey on design standards and proposed methodologies","volume":"30","author":"Bernardeschi","year":"2015","journal-title":"J. Comput. Sci. Technol."},{"key":"ref_4","unstructured":"IEC 61508-1:2010 (2010). Functional Safety of Electrical\/Electronic\/Programmable Electronic Safety-Related Systems, International Electrotechnical Commission. [2nd ed.]."},{"key":"ref_5","unstructured":"Naser, J., Fink, B., Killian, C., Nguyen, T., and Druilhe, A. (2009). Guidelines on the Use of Field Programmable Gate Arrays in Nuclear Power Plant I&C Systems, EPRI."},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"75","DOI":"10.32620\/reks.2020.3.08","article-title":"Practical aspects of operating and analytical reliability assessment of FPGA-based I&C systems","volume":"3","author":"Babeshko","year":"2020","journal-title":"Radioelectron. Comput. Syst."},{"key":"ref_7","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R. (2009). Modeling in Event-B: System and Software Engineering, Cambridge University Press.","DOI":"10.1017\/CBO9781139195881"},{"key":"ref_8","unstructured":"Diller, A.Z. (1994). An Introduction to Formal Methods, Wiley."},{"key":"ref_9","unstructured":"Lecomte, T., Servat, T., and Pouzancre, G. (2007, January 29\u201331). Formal Methods in Safety-Critical Railway Systems. In Proceedings of 10th Brasilian Symposium on Formal Methods, Ouro Preto, Brazil."},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Howar, F., and Barnat, J. (2018, January 3\u20134). Formal Methods for Industrial Critical Systems. Proceedings of the 23rd International Conference on Formal Methods for Industrial Critical Systems, FMICS, Maynooth, Ireland.","DOI":"10.1007\/978-3-030-00244-2"},{"key":"ref_11","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., and Bloem, R. (2018). Handbook of Model Checking, Springer.","DOI":"10.1007\/978-3-319-10575-8"},{"key":"ref_12","doi-asserted-by":"crossref","unstructured":"Knauss, E., and Goedicke, M. (2019, January 18\u201321). Requirements Engineering: Foundation for Software Quality. Proceedings of the 25th International Working Conference, REFSQ 2019, Essen, Germany.","DOI":"10.1007\/978-3-030-15538-4"},{"key":"ref_13","first-page":"57","article-title":"A formal verification methodology for DDD mode pacemaker control programs","volume":"2015","author":"Shuja","year":"2015","journal-title":"J. Electr. Comput. Eng."},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1109\/LES.2015.2450677","article-title":"A formal verification methodology for FPGA-based stepper motor control","volume":"7","author":"Jabeen","year":"2015","journal-title":"IEEE Embed. Syst. Lett."},{"key":"ref_15","unstructured":"Bui, M., Lu, M., Hojabr, R., Chen, M., and Shriraman, A. (2020). Real-Time Formal Verification of Autonomous Systems with An FPGA. arXiv, Available online: https:\/\/arxiv.org\/pdf\/2012.04011.pdf."},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Ceesay-Seitz, K., Boukabache, H., and Perrin, D. (2020, January 16\u201318). A Functional Verification Methodology for Highly Parametrizable, Continuously Operating Safety-Critical FPGA Designs: Applied to the CERN RadiatiOn Monitoring Electronics (CROME). Proceedings of the International Conference on Computer Safety, Reliability, and Security, Lisbon, Portuga.","DOI":"10.1007\/978-3-030-54549-9_5"},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"113492","DOI":"10.1016\/j.microrel.2019.113492","article-title":"Fault Resilient FPGA Design for 28 nm ZYNQ System-on-Chip Based Radiation Monitoring System at CERN","volume":"100\u2013101","author":"Toner","year":"2019","journal-title":"Microelectron. Reliab."},{"key":"ref_18","unstructured":"Pakonen, A., Tahvonen, T., Hartikainen, M., and Pihlanko, M. (2017, January 11\u201315). Practical applications of model checking in the Finnish nuclear industry. Proceedings of the 10th International Topical Meeting on Nuclear Plant Instrumentation, Control and Human Machine Interface Technologies (NPIC & HMIT 2017), San Francisco, CA, USA."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/j.ress.2020.107237","article-title":"Model checking reveals design issues leading to spurious actuation of nuclear instrumentation and control systems","volume":"205","author":"Pakonen","year":"2021","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"162139","DOI":"10.1109\/ACCESS.2019.2951938","article-title":"Model-checking detailed fault-tolerant nuclear power plant safety functions","volume":"7","author":"Buzhinsky","year":"2019","journal-title":"IEEE Access"},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1049\/iet-cdt.2016.0189","article-title":"Formal verification methodology for real-time Field Programmable Gate Array, IET","volume":"11","author":"Jabeen","year":"2017","journal-title":"Comput. Digit. Tech."},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"710","DOI":"10.1007\/s10559-020-00289-8","article-title":"Modeling method for development of digital system algorithms based on programmable logic devices","volume":"56","author":"Kharchenko","year":"2020","journal-title":"Cybern. Syst. Anal."},{"key":"ref_23","first-page":"1236","article-title":"FPGA trojans through detecting and weakening of cryptographic primitives","volume":"34","author":"Swierczynski","year":"2015","journal-title":"IEEE TCAD"},{"key":"ref_24","unstructured":"Booch, G., Rumbaugh, J., and Jacobson, I. (2008). Unified Modeling Language User Guide, Addison-Wesley."},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"Coelho, D. (1989). The VHDL Handbook, Springer Science & Business Media.","DOI":"10.1007\/978-1-4613-1633-6"},{"key":"ref_26","unstructured":"(2021, September 10). System Verilog. Available online: www.asic-world.com\/systemverilog\/tutorial.html."},{"key":"ref_27","unstructured":"(2021, September 10). VC Formal. Available online: https:\/\/www.synopsys.com\/verification\/static-and-formal-verification\/vc-formal.html."},{"key":"ref_28","unstructured":"(2021, September 10). Vivado Verification. Available online: https:\/\/www.xilinx.com\/products\/design-tools\/vivado\/verification.html."},{"key":"ref_29","unstructured":"(2021, September 10). JasperGold. Available online: https:\/\/www.cadence.com\/ko_KR\/home\/tools\/system-design-and-verification\/formal-and-static-verification\/jasper-gold-verification-platform.html."},{"key":"ref_30","first-page":"357","article-title":"Insertion Modeling and Its Applications","volume":"24","author":"Letichevsky","year":"2016","journal-title":"Comput. Sci. J. Mold."},{"key":"ref_31","doi-asserted-by":"crossref","unstructured":"Bert, D., and Choppy, C. (1999). Interaction of agents and environments. Recent Trends in Algebraic Development Technique, Springer.","DOI":"10.1007\/b75154"},{"key":"ref_32","doi-asserted-by":"crossref","unstructured":"Kudryavtsev, V.B., and Rosenberg, I.G. (2005). Algebra of Behavior Transformations and its Applications. Structural Theory of Automata, Semigroups, and Universal Algebra, Springer.","DOI":"10.1007\/1-4020-3817-8"},{"key":"ref_33","unstructured":"(2021, September 10). ITU-T Recommendation, Z.120, Message Sequence Charts (MSC). Available online: https:\/\/www.itu.int\/rec\/dologin_pub.asp?lang=e&id=T-REC-Z.120-201102-I!!PDF-E&type=items."},{"key":"ref_34","unstructured":"Letychevskyi, O., Peschanenko, V., and Volkov, V. (October, January 28). Algebraic Virtual Machine Project. Proceedings of the17th International Conference ICTERI, Ukraine, Kherson."},{"key":"ref_35","unstructured":"Ehlers, T., Nowotka, D., and Sieweck, P. (2021, September 10). Finding Race Conditions in Real-Time Code by Using Formal Software Verification, Department of Computer Science, Kiel University. Available online: https:\/\/www.researchgate.net\/publication\/288563365_Finding_race_conditions_in_real-time_code_by_using_formal_software_verification."},{"key":"ref_36","unstructured":"Didier, J.-Y., and Mallem, M. (2021, September 10). A New Approach to Detect Potential Race Conditions in Component-Based Systems. Available online: https:\/\/hal.archives-ouvertes.fr\/hal-01024478."},{"key":"ref_37","unstructured":"Beckman, N.E. (2021, September 10). A Survey of Methods for Preventing Race Conditions. Available online: https:\/\/www.cs.cmu.edu\/~nbeckman\/papers\/race_detection_survey.pdf."},{"key":"ref_38","unstructured":"Ermolayev, V. (2015, January 14\u201316). An Interleaving Reduction for Reachability Checking in Symbolic Modeling. Proceedings of the 11th Int. Conf. ICTERI 2015, Lviv, Ukraine. Available online: Ceur-ws.org\/Vol-1356\/paper_74.pdf."},{"key":"ref_39","unstructured":"Jonson, G. (2010, January 7\u201311). The INSAG Defense in Depth Concept and D-in-D&D In Instrumentation and Control. Proceedings of 7th ANS Topical Meeting on NPIC-HMIT, Las Vegas, LA, USA."},{"key":"ref_40","unstructured":"Kharchenko, V., Bakhmach, E., and Siora, A. (2009, January 5\u20139). Diversity-scalable decisions for FPGA-based safety-critical I&C systems: From theory to implementation. Proceedings of the 6th American Nuclear Society International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies, Knoxville, TN, USA."},{"key":"ref_41","doi-asserted-by":"crossref","unstructured":"Karam, R., Hoque, T., Ray, S., Tehranipoor, M., and Bhunia, S. (2017, January 16\u201319). MUTARCH: Architectural diversity for FPGA device and IP security. Proceedings of the 2017 22nd Asia and South Pacific Design Automation Conference (ASP-DAC), Chiba City, Japan.","DOI":"10.1109\/ASPDAC.2017.7858391"},{"key":"ref_42","unstructured":"Kharchenko, V. (2020, January 12). Independent Verification and Diversity: Two Echelons of Cyber Physical Systems Safety and Security Assurance. Proceedings of the 2nd International Workshop on Information-Communication Technologies & Embedded Systems (ICTES 2020), Mykolaiv, Ukraine. Available online: Ceur-ws.org\/Vol-2762\/invited2.pdf."},{"key":"ref_43","unstructured":"Kharchenko, V., Siora, A., Sklyar, V., Volkoviy, A., and Bezsaliy, V. (2010, January 7\u201311). Multi-diversity versus common cause failures: FPGA-based multi-version NPP I&C systems. Proceedings of the 7th International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies 2010, NPIC and HMIT, Las Vegas, NV, USA."},{"key":"ref_44","unstructured":"Eriksson, J. (2010). Tool-Supported Invariant-Based Programming. [Ph.D. Thesis, \u00c5bo Akademi University]."},{"key":"ref_45","doi-asserted-by":"crossref","unstructured":"Kharchenko, V., Konorev, B., Sklyar, V., and Reva, L. (2013, January 27\u201330). Invariant-oriented verification of HDL-based safety critical systems. Proceedings of the East-West Design & Test Symposium (EWDTS 2013), Rostov on Don, Russia.","DOI":"10.1109\/EWDTS.2013.6673160"},{"key":"ref_46","unstructured":"Ostroumov, S., and Tsiopoulos, L. (September, January 31). VHDL Code Generation from Formal Event-B Models. Proceedings of 4th Euromicro Conference on Digital System Design, Oulu, Finland."},{"key":"ref_47","doi-asserted-by":"crossref","unstructured":"Petre, L., Sere, K., and Troubitsyna, E. (2012). Towards Designing FPGA-Based Systems by Refinement in B. Dependability and Computer Engineering: Concepts for Software-Intensive Systems, IGI Global.","DOI":"10.4018\/978-1-60960-747-0"},{"key":"ref_48","doi-asserted-by":"crossref","unstructured":"Andrashov, A., Kharchenko, V., Sklyar, V., Reva, L., Dovgopolyi, V., and Golovir, V. (2010, January 17\u201320). Verification of FPGA electronic designs for nuclear reactor trip systems: Test- and invariant-based methods. Proceedings of the 2010 East-West Design & Test Symposium (EWDTS), St. Petersburg, Russia.","DOI":"10.1109\/EWDTS.2010.5742120"},{"key":"ref_49","doi-asserted-by":"crossref","first-page":"52","DOI":"10.32918\/nrs.2020.2(86).07","article-title":"Application of the FPGA Technology for the Development of Multi-Version Safety-Critical NPP Instrumentation and Control Systems","volume":"2","author":"Perepelitsyn","year":"2020","journal-title":"Nucl. Radiat. Saf."},{"key":"ref_50","doi-asserted-by":"crossref","unstructured":"Kharchenko, V., and Illiashenko, O. (2016, January 14\u201317). Diversity for security: Case assessment for FPGA-based safety-critical systems. Proceedings of the MATEC Web of Conferences 20th International Conference on Circuits, Systems, Communications and Computers (CSCC 2016), Corfu Island, Greece.","DOI":"10.1051\/matecconf\/20167602051"},{"key":"ref_51","doi-asserted-by":"crossref","unstructured":"Illiashenko, O., Kharchenko, V., Kor, A.-L., Panarin, A., and Sklyar, V. (2017, January 21\u201323). Hardware diversity and modified NUREG\/CR-7007 based assessment of NPP I&C safety. Proceedings of the IEEE 9th International Conference on Intelligent Data Acquisition and Advanced Computing Systems: Technology and Applications, IDAACS, Bucharest, Romania.","DOI":"10.1109\/IDAACS.2017.8095218"},{"key":"ref_52","unstructured":"IEEE (2019). 1076-2019\u2014IEEE Standard for VHDL Language Reference Manual, IEEE."},{"key":"ref_53","doi-asserted-by":"crossref","first-page":"119","DOI":"10.32620\/reks.2021.1.11","article-title":"Hyper redundancy for super reliable FPGAs","volume":"1","author":"Tyurin","year":"2021","journal-title":"Radioelectron. Comput. Syst."}],"container-title":["Computers"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-431X\/10\/10\/125\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T07:11:20Z","timestamp":1760166680000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-431X\/10\/10\/125"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,10]]},"references-count":53,"journal-issue":{"issue":"10","published-online":{"date-parts":[[2021,10]]}},"alternative-id":["computers10100125"],"URL":"https:\/\/doi.org\/10.3390\/computers10100125","relation":{},"ISSN":["2073-431X"],"issn-type":[{"type":"electronic","value":"2073-431X"}],"subject":[],"published":{"date-parts":[[2021,10,10]]}}}