V.V. Shkarupylo, V.V. Dusheba, S.Yu. Skrupsky, I.V. Blinov
Èlektron. model. 2022, 44(2):90-89
https://doi.org/10.15407/emodel.44.02.090
ABSTRACT
Design is approached as a stage of the engineering process represented as the following sequence: requirements analysis, design, implementation, validation. Validation, in its turn, can be implemented both by way of simulation and by way of testing. Safety-critical system is approached as a system whose functioning faults and failures can lead to critical consequences. In this paper, an attention is focused on the program level — the program-algorithmic constituent. In this scope, the concept of an "artifact" is utilized — an entity with architecture and content; an outcome of certain step within the design stage, formalized appropriately — in the form of an algorithm flowchart, diagram, formalized representation. The idea behind the presented work is to control the indicators of not only functional properties, but also non-functional properties at the design stage of engineering process — on the basis of the named artifacts. The latter, in turn, are typically checked at the final validation stage of engineering process. Carrying out stressed control is a way to foster the increase of the level of system under development functional safety by addressing the software and algorithmic plane. It is proposed to achieve so by deploying the mechanism of artifacts inheritance: initial artifacts, which consistencies are considered and confirmed as an indicator of functional properties at the design stage of engineering process, are positioned as source constructs, the derivative artifacts (formalized representations) are synthesized from. To provide such an instrument, a hierarchical model of non-functional properties representation is described in given paper. Named model is devoted to serve as a prototype – a unification mechanism — providing the representation of non-functional properties at the design stage of engineering process. The Discrete Event System Specification mathematical apparatus, by Bernard P. Zeigler, is utilized for this purpose.
KEYWORDS
Discrete Event System Specification, artifact, non-functional properties, design, safety-critical system
REFERENCES
- Knight, J.C. (2002), “Safety Critical Systems: Challenges and Directions”, Software Engineering: proceedings of the 24th International Conference, ICSE '02, Orlando, FL, pp. 547-550, available at: https://doi.org/10.1145/581339.581406 (accessed: 08 April 2022).
https://doi.org/10.1145/581339.581406 - Shkarupylo, V.V., Kudermetov, R.K. and Polska O.V. (2018), “On the approaches to cyber-physical systems simulation”, Advances in Cyber-Physical Systems (ACPS), Vol. 3, no. 1, pp. 51-54, available at: https://doi.org/10.23939/acps2018.01.051 (accessed: 08 April 2022).
https://doi.org/10.23939/acps2018.01.051 - Kyrylenko, A.V. (2014), Intellektualnyye elektroenergeticheskiye sistemy: elementy i rezhimy [Intelligent power systems: elements and modes], Institut elektrodinamiki NAN Ukrainy, Kyiv, Ukraine.
- Kyrylenko, O.V., Blinov, I.V. and Tankevych, S.E. (2012), “Smart grid and organization of information exchange in electric power systems”, Tekhnichna elektrodynamika, 3, pp. 44-54.
- ІEC/TR 63097:2017, Smart grid standardization roadmap (2017), available at: https:// iteh.ai/catalog/standards/iec/f3bffb16-2681-4e9f-890a-d63ed6c010cf/iec-tr-63097-2017 (accessed: 10 April 2022).
- Ding, D., Han, Q.-L., Wang, Z. and Ge, X. (2019), “A Survey on Model-Based Distributed Control and Filtering for Industrial Cyber-Physical Systems”, IEEE Transactions on Industrial Informatics, Vol. 15, no. 5, pp. 2483-2499, available at: https://doi.org/10.1109/ 2019.2905295 (accessed: 08 April 2022).
https://doi.org/10.1109/TII.2019.2905295 - Resch, S. and Paulitsch, M. (2017), “Using TLA+ in the Development of a Safety-Critical Fault-Tolerant Middleware”, Software Reliability Engineering Workshops: 2017 IEEE International Symposium, Toulouse, France, pp. 146-152, available at: https:// doi.org/10.1109/ISSREW.2017.43 (accessed: 08 April 2022).
https://doi.org/10.1109/ISSREW.2017.43 - Lamport, L. (2002), Specifying systems: The TLA+ language and tools for hardware and software engineers, Addison-Wesley, Boston, MA.
- Railway applications — Communication, signalling and processing systems - Software for railway control and protection systems (CENELEC - EN 50128), by European Committee for Electrotechnical Standardization (CENELEC), June 2020, available at: https:// globalspec.com/std/14317747/EN%2050128 (accessed: 08 April 2022).
- On approval of the Requirements on nuclear and radiation safety to information and control systems important for the safety of nuclear power plants: Order of the State Inspectorate for Nuclear Regulation dated 22.07.2015 № 140 as amended in accordance with the Order of the State Inspectorate for Nuclear Regulation № 508 dated 25.11.2019, available at: https://zakon.rada.gov.ua/laws/term/34229 (accessed: 08 April 2022).
- Broy, M. (2013), “A logical approach to systems engineering artifacts and traceability: from requirements to functional and architectural views. Engineering dependable software systems: NATO Science for Peace and Security Series”, Information and Communication Security, Vol. 34. pp. 1-48, available at: https://doi.org/10.3233/978-1-61499-207-3-1 (accessed: 08 April 2022).
- Shkarupylo, V.V. and Blinov, I.V. (2021), Stsenarii, metody ta zasoby formalnoi veryfikatsii artefaktiv protsesu proiektuvannia system krytychnoho pryznachennia: monohrafiia [Scenarios, methods and means of formal verification of artifacts of the process of designing critical systems], HO «Yevropeyska naukova platforma», Vinnytsya, Ukraine, available at: https://doi.org/10.36074/smtzfvappskp-monograph.2021 (accessed: 08 April 2022).
https://doi.org/10.36074/smtzfvappskp-monograph.2021 - Shkarupylo, V., Alsayaydeh, J.A.J, Tomičić, I., Chemeris, A. and Dusheba, V. (2021), “A technique for checking the adequacy of formal model”, ARPN Journal of Engineering and Applied Sciences, Vol. 16, no. 16, pp. 1707-1719, available at: http://www.arpnjournals.org/ jeas/research_papers/rp_2021/jeas_0821_8670.pdf (accessed: 08 April 2022).
- Shkarupylo, V.V., Chemerys, O.A., Dusheba, V.V., Kudermetov, R.K. and Polska, O.V. (2021), “Model-driven approach to non-functional properties indexes control at design”, Vcheni zapysky Tavriiskoho natsionalnoho universytetu imeni V.I. Vernadskoho, seriia «Tekhnichni nauky», Vol. 32, no. 71/1, pp. 166-171, available at: https://doi.org/ 32838/2663-5941/2021.1-1/27 (accessed: 08 April 2022).
https://doi.org/10.32838/2663-5941/2021.1-1/27 - Shkarupylo, V. (2016), “A Technique of DEVS-Driven Validation”, In Modern Problems of Radio Engineering, Telecommunications, and Computer Science: XIIIth Int. Conf., TCSET'2016, Lviv-Slavske, Ukraine, pp. 495-497, available at: https://doi.org/ 10.1109/TCSET.2016.7452097 (accessed: 08 April 2022).
https://doi.org/10.1109/TCSET.2016.7452097 - Van Tendeloo, Y. and Vangheluwe, H. (2017), “An evaluation of DEVS simulation tools”, SIMULATION, Vol. 93, no. 2, pp. 103-121, available at: https://doi.org/10.1177/ 0037549716678330 (accessed: 08 April 2022).
https://doi.org/10.1177/0037549716678330 - Van Tendeloo, Y. and Vangheluwe, H. (2018), “Discrete event system specification modeling and simulation”, Proceedings of the 2018 Winter Simulation Conference, Gothenburg, Sweden, pp. 162-176, available at: https://doi.org/10.1109/WSC.2018.8632372 (accessed: 08 April 2022).
- Shkarupylo, V.V., Kudermetov, R.K. and Polska, O.V. (2015), “DEVS-oriented technique for composite web services validity checking”, Radioelektronika, informatyka, upravlinnya, Vol. 4, pp. 79–86, available at: 10.15588/1607-3274-2015-4-12 (accessed: 08 April 2022).
- Shkarupylo, V. (2016), “A Simulation-driven Approach for Composite Web Services Validation”, 27th Int. Central European Conference on Information and Intelligent Systems, CECIIS 2016, Varazdin, Croatia, pp. 227-231, available at: http://archive.ceciis. foi.hr/app/public/conferences/1/ceciis2016/papers/QoS-1.pdf (accessed: 08 April 2022).
- Tudose, C. (2020), JUnit in Action: Third Edition, Manning Publications Co, NY, USA, ISBN 9781617297045.
- Falcone, Y., Krstić, S., Reger, G. and Traytel, D. (2021), “A taxonomy for classifying runtime verification tools”, International Journal on Software Tools for Technology Transfer, Vol. 23, pp. 255-284, available at: https://doi.org/10.1007/s10009-021-00609-z (accessed: 08 April 2022).
https://doi.org/10.1007/s10009-021-00609-z - Cohen E. et al. (2009), “VCC: A Practical System for Verifying Concurrent C”, Theorem Proving in Higher Order Logics. TPHOLs 2009, Lecture Notes in Computer Science, Berlin, Heidelberg, Springer, Vol. 5674, 23-42, available at: https://doi.org/10.1007/978-3-642-03359-9_2 (accessed: 08 April 2022).
https://doi.org/10.1007/978-3-642-03359-9_2 - Nardone, V., Santone, A., Tipaldi, M., Liuzza, D. and Glielmo, L. (2019), “Model checking techniques applied to satellite operational mode management”, IEEE Systems Journal, Vol. 13, no. 1, pp. 1018-1029, available at: https://doi.org/10.1109/JSYST.2018. 2793665 (accessed: 08 April 2022).
https://doi.org/10.1109/JSYST.2018.2793665 - Jenihhin, M., Lai, X., Ghasempouri, T. and Raik, J. (2018), “Towards multidimensional verification: where functional meets non-functional”, NORCHIP and International Symposium of System-on-Chip (SoC): 2018 IEEE Nordic Circuits and Systems Conference, Tallinn, Estonia, pp. 1-7, available at: https://arxiv.org/ftp/arxiv/papers/1908/ 1908.00314.pdf (accessed: 08 April 2022).
https://doi.org/10.1109/NORCHIP.2018.8573495 - Larman, C. (2004), Applying UML and Patterns: An Introduction to Object-Oriented Analysis and Design and Iterative Development, 3rd Edition, Pearson, available at: https://www.amazon.com/Applying-UML-Patterns-Introduction-Object- Oriented/dp/0131489062 (accessed: 08 April 2022).
- Blinov, I. and Tankevych, S. (2016), “The harmonized role model of electricity market in Ukraine”, 2nd International Conference on Intelligent Energy and Power Systems, IEPS 2016 Conference Proceedings, available at: https://doi.org/10.1109/IEPS.2016.7521861 (accessed: 08 April 2022).
https://doi.org/10.1109/IEPS.2016.7521861 - Lamport, L. (2009), “The PlusCal algorithm language”, Theoretical Aspects of Computing: 6th Int. Colloquium, part of LNCS, Kuala Lumpur, Malaysia, Vol. 5684, pp. 36-60, available at: https://lamport.azurewebsites.net/pubs/pluscal.pdf (accessed: 08 April 2022).
https://doi.org/10.1007/978-3-642-03466-4_2 - Shkarupylo, V.V. and Blinov, I.V. (2021), “Model-oriented approach to the formalization of non-functional characteristics of critical systems, in particular in nature management”, Hlobalni ta rehionalni problemy informatyzatsiyi v suspilstvi i pryrodokorystuvanni 2021: IX Mizhnarodna naukovo-praktychna Internet-konferentsiya [Global and regional problems of informatization in society and nature using ‘2021: IX International scientific Internet conference], Kyiv, Ukraine, NUBiP, May 13-14, 2021, pp. 55-57.
- Shkarupylo, V., Chemeris, A., Dusheba, V., Kudermetov, R. and Polska, O. (2020), “Method for formal specifications synthesis on the basis of Hoare triples”, Scientific papers of Donetsk National Technical University: Informatics, Cybernetics and Computer Science, Vol. 1, no. 30, pp. 49-57, available at: https://iktv.donntu.edu.ua/wp-content/uploads/ 2021/01/07_Shkarupylo.pdf (accessed: 08 April 2022).
- Clarke, E.M., Grumberg, O., Kroening, D., Peled, D. and Veith, H. (2018), Model checking, 2nd ed., The MIT Press, MA, USA, available at: https://mitpress.mit.edu/books/model- checking-second-edition (accessed: 08 April 2022).
- Shkarupylo, V.V. and Dusheba, V.V. (2021), “Approach to the synthesis of formalized representations of non-functional characteristics at the design stage”, Bezpeka enerhetyky v epokhu tsyfrovoi transformatsii: III naukovo-praktychna konferentsiia Instytutu problem modeliuvannia v enerhetytsi im. H.Ye. Pukhova Natsionalnoi akademii nauk Ukrainy [Energy security in the age of digital transformation. III scientific-practical conference of the Institute of Modeling Problems in Energy named after G.Ye. Pukhov NASU], Kyiv, Ukraine, IPME im. H.Ye. Pukhova NAN Ukrayiny, December 22, 2021, pp. 128-130.
- Shkarupylo, V.V., Blinov, I.V., Chemeris, A.A., Dusheba, V.V. and Alsayaydeh J.A.J. (2022), “On Applicability of Model Checking Technique in Power Systems and Electric Power Industry”, Studies in Systems, Decision and Control, Vol. 399, available at: https://doi.org/10.1007/978-3-030-87675-3_1 (accessed: 08 April 2022).
https://doi.org/10.1007/978-3-030-87675-3_1 - Mesarovic, M.D., Macko, D. and Takahara, Y. (1970), Theory of hierarchical, multilevel, systems, Academic Press, NY, USA.
- Blinov, I.V. (2021), “Problems of functioning and development of a new electricity market model in Ukraine”, Visnyk NAN Ukrayiny, Vol. 3, pp. 20-28, available at: https:// org/10.15407/visn2021.03.020 (accessed: 08 April 2022).
https://doi.org/10.15407/visn2021.03.020 - Blinov, I.V., Parus, E.V. and Shkarupylo, V.V. (2021), Struktura ta modeli informatsiynoyi vzayemodiyi uchasnykiv rynku elektrychnoyi enerhiyi [Structure and models of information exchange of electricity market participants], HO «Yevropeyska naukova platforma», Vinnytsya, Ukraine.