Traversal of arbitrary sequences of UCM symbolic transitions for test generation

Traversal of arbitrary sequences of UCM symbolic transitions for test generation

The paper proposes a method of traversal of high-level multi-threaded models formalized in UCM language. The pros and cons of this approach comparing to the existing ones are considered. The method that allows state space exploring of UCM models using symbolic solving and proving is presented. The g...

Повний опис

Збережено в:
Бібліографічні деталі
Дата:2025
Автор: Guba, A.A.
Формат: Стаття
Мова:English
Опубліковано: Інститут програмних систем НАН України 2025
Теми:
UDC 004.415.5
Онлайн доступ:https://pp.isofts.kiev.ua/index.php/ojs1/article/view/701
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Problems in programming

Репозитарії

Problems in programming
id pp_isofts_kiev_ua-article-701
record_format ojs
resource_txt_mv ppisoftskievua/6f/bd3a107717e936f287b1f3ede0dd126f.pdf
spelling pp_isofts_kiev_ua-article-7012025-04-09T22:22:32Z Traversal of arbitrary sequences of UCM symbolic transitions for test generation Traversal of arbitrary sequences of UCM symbolic transitions for test generation Guba, A.A. UDC 004.415.5 УДК 004.415.5 The paper proposes a method of traversal of high-level multi-threaded models formalized in UCM language. The pros and cons of this approach comparing to the existing ones are considered. The method that allows state space exploring of UCM models using symbolic solving and proving is presented. The generation of symbolic traces used for software system testing is described.Prombles in programming 2014; 2-3: 107-111 Запропоновано метод обходу високорівневих багатопотокових моделей, які формалізовані мовою UCM. Розглядаються переваги та недоліки даного підходу у порівнянні з існуючими. Представлений метод дозволяє обходити простір станів моделей UCM, використовуючи символьне розв’язання та доведення. Описана генерація символьних трас, які використовуються для тестування програмних систем. Prombles in programming 2014; 2-3: 107-111  Інститут програмних систем НАН України 2025-04-09 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/701 PROBLEMS IN PROGRAMMING; No 2-3 (2014); 107-111 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2014); 107-111 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2014); 107-111 1727-4907 en https://pp.isofts.kiev.ua/index.php/ojs1/article/view/701/753 Copyright (c) 2025 PROBLEMS IN PROGRAMMING
institution Problems in programming
baseUrl_str https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date 2025-04-09T22:22:32Z
collection OJS
language English
topic
UDC 004.415.5
spellingShingle
UDC 004.415.5
Guba, A.A.
Traversal of arbitrary sequences of UCM symbolic transitions for test generation
topic_facet
UDC 004.415.5

УДК 004.415.5
format Article
author Guba, A.A.
author_facet Guba, A.A.
author_sort Guba, A.A.
title Traversal of arbitrary sequences of UCM symbolic transitions for test generation
title_short Traversal of arbitrary sequences of UCM symbolic transitions for test generation
title_full Traversal of arbitrary sequences of UCM symbolic transitions for test generation
title_fullStr Traversal of arbitrary sequences of UCM symbolic transitions for test generation
title_full_unstemmed Traversal of arbitrary sequences of UCM symbolic transitions for test generation
title_sort traversal of arbitrary sequences of ucm symbolic transitions for test generation
title_alt Traversal of arbitrary sequences of UCM symbolic transitions for test generation
description The paper proposes a method of traversal of high-level multi-threaded models formalized in UCM language. The pros and cons of this approach comparing to the existing ones are considered. The method that allows state space exploring of UCM models using symbolic solving and proving is presented. The generation of symbolic traces used for software system testing is described.Prombles in programming 2014; 2-3: 107-111
publisher Інститут програмних систем НАН України
publishDate 2025
url https://pp.isofts.kiev.ua/index.php/ojs1/article/view/701
work_keys_str_mv AT gubaaa traversalofarbitrarysequencesofucmsymbolictransitionsfortestgeneration
first_indexed 2025-07-17T10:03:05Z
last_indexed 2025-07-17T10:03:05Z
_version_ 1838410407341981696
fulltext Методи та засоби програмної інженерії © А.А. Guba, 2014 ISSN 1727-4907. Проблеми програмування. 2014. № 2–3. Спеціальний випуск 107 UDC 004.415.5 TRAVERSAL OF ARBITRARY SEQUENCES OF UCM SYMBOLIC TRANSITIONS FOR TEST GENERATION A.A. Guba Glushkov Institute of Cybernetics of NAS of Ukraine, 40 Glushkova ave., Kyiv, Ukraine, 03680. Tel.: (044) 526 0058, E-mail: antonguba@ukr.net The paper proposes a method of traversal of high-level multi-threaded models formalized in UCM language. The pros and cons of this approach comparing to the existing ones are considered. The method that allows state space exploring of UCM models using symbolic solving and proving is presented. The generation of symbolic traces used for software system testing is described. Запропоновано метод обходу високорівневих багатопотокових моделей, які формалізовані мовою UCM. Розглядаються переваги та недоліки даного підходу у порівнянні з існуючими. Представлений метод дозволяє обходити простір станів моделей UCM, використовуючи символьне розв’язання та доведення. Описана генерація символьних трас, які використовуються для тестування програмних систем. Introduction Use Case Map (UCM) is a scenario based language that has associated behavior of the system with its architec- ture in the formal and visual forms. It has been successfully used in describing real-time systems, with a particular focus on telecommunication system and services. UCM is a part of an approved proposal to ITU-T for a User Requirements Notation (URN) [1]. It can be applied to capture and integrate functional requirements in terms of causal scenarios rep- resenting behavioral aspects at a higher level of abstraction, and to provide the reasoning about the system architecture and behavior. UCM is not intended to replace UML, but rather complement it and help to bridge the modeling gap be- tween requirements (use cases) and design (system components and behavior). UCM semantics began to develop in the early 1990s . The first attempt to construct the semantics of UCM was the introduction of a traversal mechanism for UCM [2, 3], which allows you to select a specific scenario in the language of UCM model and convert it to MSC [4]. Later, UCM semantics was expressed by LOTOS language formalisms [5], abstract state machines (ASM) [6], as well as timed transition systems (CTS) and timed automata (TA) [7]. Recent works on the semantics of UCM based on the modeling of business processes [8] and use the theory of Petri nets [9]. In [10, 11] an insertional model was used as the formalism for describing the semantics of UCM. The traversal of UCM use deductive symbolic simulation tools together with the modeling of the behavior of a system using model checking. This paper is the continuation of [10, 11] and enhances the usage of sequences of UCM language constructs, as well as proposes an approach for trace generation of high-level multi-threaded UCM with arbitrary UCM constructs connection types. Some methods of implementation of UCM semantics are compared. UCM specification UCM specification (UCM project) is a set of UCM maps, which consist of a finite, possibly empty set of UCM paths. Maps are the basic notion of the language and express behavior scenario. Maps are represented as graph struc- tures, which vertices are associated with language constructs. Paths define the order of the vertices. Vertices can be con- structs of different types used to express start and end of paths, alternative and parallel branches, merging of paths. Path is located on different maps, which could be linked by vertices of stub type [11]. Vertices can be inside the component. The components are abstract entities that are used to express the structure of the model, and could be nested into another component. UCM specifications are suitable to describe multithreaded systems. Multithreaded system is a system of interacting parallel processes in which interaction takes place via shared memory. An example of such system could be programs for multicore processors. Multithreading in UCM is implemented by parallel paths and parallel branches. In this paper, the following UCM constructs are considered:  StartPoint (beginning of a path),  EndPoint (end of a path),  EmptyPoint (empty construct),  DirectionArrow (indication of a path direction),  Responsibility (action, some operator),  OrFork (alternative branching),  OrJoin (joining of alternatives without synchronization),  AndFork (parallel branching),  AndJoin (joining of parallel alternatives with synchronization),  WaitingPlace (waiting condition),  Stub (link from one UCM map to another). mailto:antonguba@ukr.net Методи та засоби програмної інженерії 108 Fig.1. Example of UCM map The meaning of UCM project is a transition system represented as a composition of multilevel UCM environ- ment and agents inserted into this environment at different levels. The structure of the UCM environment is defined by the environment description. Agents correspond to components. Environment is specified by attributes definition. There are global and local attributes. Besides attributes classification with respect to level of localization, it is considered their division into two disjoint classes of attributes: user-defined (data flow) and control (control flow). User-defined attrib- utes are introduced by UCM developer and are used in Responsibility and WaitingPlace. Control attributes are formed at the stage of model construction from UCM project – translation of the project to the system of environment and agents in order to provide synchronization of processes corresponding to the semantics defined in [10, 11], and could be efficiently realized in C++ code as it was shown in [12]. Basic protocols language The language, which is used for describing formulas with user-defined attributes (conditions, assignments, etc.) is called Basic Protocols Language. A basic protocol is a formula of dynamic logic )),(),(),(( rxrxPrxx   and describes the local properties of a system in terms of pre- and postconditions α and β. Both are formulae of first order multisorted logic interpreted on a data domain, P is a process, represented by means of an MSC diagram, and de- scribes the reaction of a system triggered by the precondition, x is a set of typed data variables, and r is a set of envi- ronment and agent attributes. The general theory of basic protocols is presented in [13]. At transitions in the space of formulas, a postcondition is considered as an operator. As the operator transforms one formula to another, in [14] a term “predicate transformer” was used. Thus, to compute transitions between the states of such models, basic protocols are interpreted as predicate transformers: for a given symbolic state of a system and a given basic protocol, the direct predicate transformer generates the next symbolic state as its strongest postcondition and the backward predicate transformer generates the previous symbolic state as its weakest precondition. These concepts have been implemented in VRS (Verification of Requirement Specifications) and IMS (Insertion Modeling System) systems [15]. The following data types in the models are supported:  simple data types: Boolean, integer, real, enumerated, and symbolic,  structured data types: uninterpreted functional symbols, arrays, and lists of simple date types. Symbolic type is represented by expression in algebra of free terms. Enumerated type is a user-defined one con- tains symbolic constants (atomic expressions in algebra of free terms). Parameters and returned value of uninterpreted functional symbols are simple data types only. Let denote that if we are talking about functional, then we mean uninter- preted functional symbol. Arrays are considered as uninterpreted functional symbols with bound restrictions for values of parameters. Let E(r) be an environment state. Application of a basic protocol to an environment state looks like the following formula: )),,(),,()(())),()()(,(( rxrxrEptxrxrErx   where pt is a function of predicate transformer. In general, a postcondition of basic protocol can be considered as fol- lowing conjunction: Методи та засоби програмної інженерії 109 ),(),(),(),( rxCrxLrxArx  , where ),( rxA is a conjunction of assignments, ),( rxL is a conjunction of list operators add_to_tail, add_to_head, ),( rxC is a formula part of postcondition. Automatic test generation UCM language makes development of projects user-convenient. It is easy to add new maps and paths to existing project. Such method of incremental system design provides rich opportunities for developers, but at the same time, it may lead to errors in the early stages of system development. Detection of errors in early stages of the project develop- ment greatly reduces the number of product corrections and total cost of software development. Therefore, methods of testing and model-based testing tools have been actively developed. This paper is devoted to the enhancement of automatic test technology for VRS/TAT [16] toolkit that supports automatic generation of test scenarios for requirements specifications specified in the notation of basic protocols. In [17] an approach of automatic translation of UCM to Basic Protocols was proposed. This approach proves to be a good engineering solution, as it does not require a lot of time of development and ensures the correct behavior of the model obtained after translation. The cons of this approach are generation of additional basic protocols, which cause:  additional calls of solver due to checks of satisfiability of pre-condition of generated protocol and envi- ronment state (performance issue),  additional calls of predicate transformer due to applying post-condition of generated protocol (perfor- mance issue),  additional stored states after application of generated protocols for visited and cycle detection (memory issue)  increase the explosion of states number if generated protocols are occurred on parallel branches (per- formance issue) Therefore, the traversal of UCM maps without generation of additional protocols becomes an actual task. From the standpoint of system behavior analyzing the notion of a path is important for testing and verification. Path p is a sequence of protocols corresponds to UCM constructs (UC): nuuup  ...21 , where UCui  , 1u – StartPoint, nu – EndPoint, ji uu  indicates that protocol corresponds to ju construct is applied after protocol corresponds to iu construct. Let us show that traversal of UCM maps and generation of valid UCM paths for system testing is possible with- out generation of additional protocols. Let us divide all UCM constructs (UC set) into three disjoint sets PC (protocol constructs), AC (auxiliary constructs), IC (intermediate constructs). Set PC shall contain UCM constructs, which have basic protocol in attachment: Responsibility and Waiting- Place. Also, we consider WaitingPlace as 3 different constructs: WaitingPlace without trigger, WaitingPlace with trigger of transient type, WaitingPlace with trigger of persistent type, because they all have different behavior. These all proto- cols are user-defined. Set AC shall contain StartPoint, EndPoint, which indicate start and end of path. StartPoint shall be used to set ini- tial model behavior for UCM traversal. EndPoint shall be used to determine the correct end of model behavior. Set IC shall contain OrFork, AndFork, AndJoin, Stub, EmptyPoint connected with WaitingPlace with trigger of transient type, EmptyPoint connected with WaitingPlace with trigger of persistent type. Stub shall be considered as a set of in/out paths. Each in-path is bound with connected StartPoint. Each out-path is bound with connected EndPoint. Thus, set IC shall contain connected StartPoint and connected EndPoint instead of Stub. DirectionArrow, OrJoin, not connected EmptyPoint shall be eliminated, because they do not affect behavior of the system. Also, let us introduce special intermediate Fake constructs (FC set) with bound empty basic protocol. Fake con- struct shall be used to transmit an environment state. It does not have any behavior semantics and just a technical tem- porary construct, which shall be eliminated together with empty protocols at the end of algorithm. Let us introduce following types of UCM transitions: 1. i s u – first transition (initialization), indicates that protocol iu is applied after StartPoint, FCPCui  , 2. e iu  – last transition (leads to path end), indicates that EndPoint is occurred after application of proto- col iu , FCPCui  , 3. ji uu  – transition indicates that protocol ju is applied after protocol iu , FCPCuu ji , , 4. j c i uu  – transition indicates that protocol ju is applied after protocol iu with the influence of seman- tics of UCM construct c, ICcFCPCuu ji  ,, . Методи та засоби програмної інженерії 110 5. j c i uu k  – transition indicates that protocol ju is applied after protocol iu with the influence of seman- tics of sequence of UCM constructs c, ICcFCPCuu ji  ,, , k –number of UCM constructs in the sequence (sequence depth). If k=0, then this is a transition of the type 3. If k=1, then this is a transition of the type 4. Definition. Two UCM paths 21, pp are called equivalent ( 21 pp  ) if they pass through the same non-empty protocol constructs and have the same environment states after application of these protocols. Lemma. Paths 211 pcpcp  and 212 pcfcpcp  are equivalent, where FCfcPCpcpc  ,, 21 . Proving. Paths consist from transitions. Path p1 consists from one transition and p2 consists from two transitions. Let us write each transition in the terms of transition rule of transition system. P1 looks like: ][][ , ')( ')()( 1 11 aEaE aaEE pcapply pcapplypcapply      , where E is an environment state before application of 1pc , E – environment state after application of pc1 and 2pc is applicable for 'E , ][aE is an insertion function, which describes interaction between environment and agent a inserted into this environment. In other words, insertion function calls application of basic protocols for given agent a. P2 transitions look like: ][][ , '')( ')(')( 1 11 aEaE aaEE pcapply pcapplypcapply      , ][][ , '''' '''''' aEaE aaEE   . Since fake construct has an empty bound protocol, it does not affect an environment state and ''' EE  . So, by definition, 21 pp  . Lemma is proved. Theorem. Let nuuup  ...211 , where 1..2,  niICPCui , 1u – StartPoint, nu – EndPoint. Let us denote PC constructs contained in 1p , as 1pPC and IC constructs contained in 1p , as 1pIC . Let e n ccs pcpcp k p k  ... 1 12 . Let us denote PCpcpc n ,...,1 constructs contained in 2p , as 2pPC and ICcc p ,...1 contained in 2p transitions, as 2pIC . If  1pPC 2pPC and 21 pp ICIC  , then 21 pp  . Proving. At first, let us split all transitions of the type 5 with depth 2k into k transitions of the type 4. j cccc ij c i pcfcfcpcpcpc k  ... , where FCfc . As a fake construct does not have any behavior semantics this transformation is clear and does not require an additional proof. Also, shifts of initialization from generated proto- col to the first one and finalization to the last one are obvious. So, a path is considered as a sequence of transitions in the form of deuce ji pcpc  or triple j c i pcpc  : e n cc i s pcpcpcpcp  ......212 . We shall prove that each possible transition in the form of triple of a path without generated protocols 2p is an equivalent to transition of path with generated protocols 1p . Total number of all triples is 112. It is impossible to show proof for all of them in this paper. Let us show the equivalence for one of them. Let us have a map that is linked via Stubs two times. So we have two different exits from the map. In [17] a copy of Responsibility1 is generated and two transitions are obtained: 3 )exit(EndPoint Connected 1 2 )exit(EndPoint Connected 1 2 1 , lityResponsibilityResponsibi lityResponsibilityResponsibi     Without generation of protocols it could be presented in the form of rewriting rule with deterministic choice op- erator “+” [15] and action check that verifies a stub binding: Responsibility1 = check(exit1).Responsibility2 + check(exit2).Responsibility3. Методи та засоби програмної інженерії 111 This is an equivalent transformation by rewriting rule definition. The correctness of other transformations can be proved similarly. Further, using the lemma described above, the theorem is proved. Conclusions Method of traversal of high-level multi-threaded models formalized in UCM language was proposed. The pro- posed method uses symbolic solving and proving and generates symbolic traces used for software system testing. It was implemented in VRS/TAT technological chain that makes it more convenient and efficient on projects of medium and high complexity. 1. International Telecommunications Union. Recommendation. Z.151 – User Requirements Notation (URN), 208 p. – 2008. 2. Kealey J. and Amyot D. Enhanced Use Case Map Traversal Semantics. 13th SDL Forum (SDL’07), Paris, France, Springer. – September 2007. – P. 133–149; 288 p. 3. Gunter Mussbacher. Aspect-Oriented User Requirements Notation. Thesis submitted to the Faculty of Graduate and Postdoctoral Studies in partial fulfillment of the requirements for the degree of Ph.D. in Computer Science. University of Ottawa, Ottawa, Canada, September 2010. – 334 p. 4. International Telecommunications. Union. Recommendation Z.120 – Message Sequence Charts (MSC), 1998. – 136 p. 5. Guan R. From Requirements to Scenarios through Specifications: A Translation Procedure from Use Case Maps to LOTOS. M.Sc. thesis, OCICS, University of Ottawa, Canada, 2002. – 146 p. 6. Hassine J., Rilling J., and Dssouli R. An ASM Operational Semantics for Use Case Maps // 13th IEEE International Requirement Engineering Conference (RE’05), IEEE Computer Society Press, September 2005. – P. 467–468; 494 p. 7. Jameleddine Hassine. Formal semantics and verification of use case maps, A thesis in The Department of Computer Science and Software En- gineering, Concordia University, Montreal, Quebec, Canada, 2008. – 299 p. 8. Weiss M. and Amyot D. Business Process Modeling with URN. International Journal of E-Business Research, July-September 2005. – Vol. 1(3). – P. 63–90; 112 p. 9. Peter Huber, Kurt Jensen, and Robert M. Shapiro. Hierarchies in coloured petri nets // In Proceedings of the 10th International Conference on Applications and Theory of Petri Nets, Springer-Verlag, London, UK – 1991. – P. 313–341; 724 p. 10. Губа А.А., Шушпанов К.И. Инсерционная семантика плоских многопотоковых моделей языка UCM // Управляющие системы и машины. – 2012. – № 6. – С. 15–21. 11. Годлевский А.Б. Инсерционная семантика параллельных процедурных конструктов языка UCM // Там же, 2012. – № 6. – С. 22–34. 12. Vladimir Peschanenko, Anton Guba, Constantin Shushpanov: (en) Specializations and Symbolic Modeling. In: Ermolayev, V. et al. (eds.) Proc. 9-th Int. Conf. ICTERI, Kherson, Ukraine, Jun 19–22, 2013. – P. 490–505. 13. Letichevsky A., Kapitonova J., Volkov V., Letichevsky Jr.A., Baranov S., Kotlyarov V., Weigert T. System Specification with Basic Protocols. Cybernetics and System Analysis. – 2005. – (4), P. 3–21. 14. Letichevsky A.A., Godlevsky A.B., Letichevsky Jr. A.A., Potienko S.V. Peschanenko V.S. Properties of Predicate Transformer of VRS System. Cybernetics and System Analyses. – 2010. – (4), P. 3–16. 15. Letichevsky A., Letychevskyi O., Peschanenko V. Insertion Modeling System. In: Clarke, E.M., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS 7162, Springer Verlag, Berlin Heidelberg, 2011. – P. 262–274. 16. Baranov S.N., Drobintsev P.D., Kotlyarov V.P., Letichevsky A.A. Implementation of an integrated verification and testing technology in tele- communication project. Proceedings // IEEE Russia Northwest Section. 110 Anniversary of Radio Invention conference. S.Petyersburg, 2005. – 11 p. 17. Никифоров И.В., Петров А.В., Юсупов Ю.В. Генерация формальной модели системы по требованиям, заданным в нотации USE CASE MAPS. Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление. СПб.: Изд -во Политехнического ун-та, 2010. – № 4 (103). – С. 191–195.

Схожі ресурси