224 result(s)
Page Size: 10, 20, 50
Export: bibtex, xml, json, csv
Order by:

CNR Author operator: and / or
more
Typology operator: and / or
Language operator: and / or
Date operator: and / or
more
Rights operator: and / or
2021 Report Open Access OPEN

Quantitative security risk modeling and analysis with RisQFLan
Ter Beek M. H., Legay A., Lluch Lafuente A., Vandin A.
Domain-specific quantitative modeling and analysis approaches are fundamental in scenarios in which qualitative approaches are inappropriate or unfeasible. In this paper, we present a tool-supported approach to quantitative graph-based security risk modeling and analysis based on attack-defense trees. Our approach is based on QFLan, a successful domain-specific approach to support quantitative modeling and analysis of highly configurable systems, whose domain-specific components have been decoupled to facilitate the instantiation of the QFLan approach in the domain of graph-based security risk modeling and analysis. Our approach incorporates distinctive features from three popular kinds of attack trees, namely enhanced attack trees, capabilities-based attack trees and attack countermeasure trees, into the domain-specific modeling language. The result is a new framework, called RisQFLan, to support quantitative security risk modeling and analysis based on attack-defense diagrams. By offering either exact or statistical verification of probabilistic attack scenarios, RisQFLan constitutes a significant novel contribution to the existing toolsets in that domain. We validate our approach by highlighting the additional features offered by RisQFLan in three illustrative case studies from seminal approaches to graph-based security risk modeling analysis based on attack trees.Source: ISTI Technical Report, ISTI-2021-TR/001, pp.1–16, 2021
Project(s): CyberSec4Europe via OpenAIRE

See at: arxiv.org Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2020 Article Open Access OPEN

A framework for quantitative modeling and analysis of highly (re)configurable systems
Ter Beek M., Legay A., Lluch Lafuente A., Vandin A.
This paper presents our approach to the quantitative modeling and analysis of highly (re)configurable systems, like software product lines. Different combinations of the optional features of such systems give rise to combinatorially many individual system variants. We use a formal modeling language that allows us to model systems with probabilistic behavior, possibly subject to quantitative feature constraints, and able to dynamically install, remove or replace features. Our models are defined in the probabilistic feature-oriented language QFLan, a rich domain specific language (DSL) for systems with variability defined in terms of features. QFLan specifications are automatically encoded in terms of a process algebra whose operational behavior interacts with a store of constraints and with a semantics based on discrete-time Markov chains. Our analysis is based on statistical model checking, which allow us to scale to larger models with respect to precise probabilistic techniques. The analyses we can conduct range from the likelihood of specific behavior to the expected average cost of specific system variants. Our approach is supported by a novel Eclipse-based tool including state-of-the-art DSL utilities for QFLan as well as analysis plug-ins. We provide a number of case studies that have driven and validated the development of our framework.Source: IEEE transactions on software engineering 46 (2020): 321–345. doi:10.1109/TSE.2018.2853726
DOI: 10.1109/TSE.2018.2853726
DOI: 10.1109/tse.2018.2853726
Project(s): QUANTICOL via OpenAIRE

See at: arXiv.org e-Print Archive Open Access | IEEE Transactions on Software Engineering Open Access | ISTI Repository Open Access | Online Research Database In Technology Open Access | IEEE Transactions on Software Engineering Restricted | IEEE Transactions on Software Engineering Restricted | IEEE Transactions on Software Engineering Restricted | IEEE Transactions on Software Engineering Restricted | IEEE Transactions on Software Engineering Restricted | IEEE Transactions on Software Engineering Restricted | CNR ExploRA Restricted | IEEE Transactions on Software Engineering Restricted


2020 Article Open Access OPEN

Timed service contract automata
Basile D., Ter Beek M. H., Legay A.
We equip a recently developed model for the specification of service contracts with real-time constraints. Service contracts offer a means to define the behavioural compliance of a composition of services, typically dictated in a service-level agreement (SLA), as the fulfilment of all service requests through service offers. Depending on their granularity, SLAs vary according to the level of criticality of the involved services and also contain real-time aspects, like the services' response or expiration time. A standard method to refine a spurious service composition into a compliant one is via the synthesis of a safe orchestration, in the form of the most permissive controller from supervisory control theory. Ideally, safe orchestrations solve competition among matching service requests and offers, in light of their criticalities and their timing constraints, in the best possible way. In this paper, we introduce timed service contract automata as a novel formal model for service contracts with real-time constraints on top of services with varying levels of criticality. We also define a means to efficiently compute their composition and their safe orchestration, using the concept of zones from timed games. The innovations of our contribution are illustrated by intuitive examples and by a preliminary evaluation.Source: Innovations in systems and software engineering (Print) 16 (2020): 199–214. doi:10.1007/s11334-019-00353-3
DOI: 10.1007/s11334-019-00353-3

See at: ISTI Repository Open Access | Innovations in Systems and Software Engineering Restricted | Innovations in Systems and Software Engineering Restricted | Innovations in Systems and Software Engineering Restricted | Innovations in Systems and Software Engineering Restricted | link.springer.com Restricted | Innovations in Systems and Software Engineering Restricted | Innovations in Systems and Software Engineering Restricted | CNR ExploRA Restricted


2020 Article Open Access OPEN

Controller synthesis of service contracts with variability
Basile D., Ter Beek M. H., Degano P., Legay A., Ferrari G. L., Gnesi S., Di Giandomenico F.
Service contracts characterise the desired behavioural compliance of a composition of services. Compliance is typically defined by the fulfilment of all service requests through service offers, as dictated by a given Service-Level Agreement (SLA). Contract automata are a recently introduced formalism for specifying and composing service contracts. Based on the notion of synthesis of the most permissive controller from Supervisory Control Theory, a safe orchestration of contract automata can be computed that refines a composition into a compliant one. To model more fine-grained SLA and more adaptive service orchestrations, in this paper we endow contract automata with two orthogonal layers of variability: (i) at the structural level, constraints over service requests and offers define different configurations of a contract automaton, depending on which requests and offers are selected or discarded, and (ii) at the behavioural level, service requests of different levels of criticality can be declared, which induces the novel notion of semi-controllability. The synthesis of orchestrations is thus extended to respect both the structural and the behavioural variability constraints. Finally, we show how to efficiently compute the orchestration of all configurations from only a subset of these configurations. A prototypical tool supports the developed theory.Source: Science of computer programming (Print) 187 (2020). doi:10.1016/j.scico.2019.102344
DOI: 10.1016/j.scico.2019.102344

See at: Science of Computer Programming Open Access | Flore (Florence Research Repository) Open Access | ISTI Repository Open Access | ISTI Repository Open Access | CNR ExploRA Open Access | www.sciencedirect.com Open Access | Science of Computer Programming Restricted | Science of Computer Programming Restricted | Science of Computer Programming Restricted | Science of Computer Programming Restricted | Science of Computer Programming Restricted


2020 Conference object Open Access OPEN

Variability meets security: quantitative security modeling and analysis of highly customizable attack scenarios
Ter Beek M. H. Legay A., Lluch Lafuente A., Vandin A.
We present a framework for quantitative security modeling and analysis of highly customizable attack scenarios, which resulted as a spin-off from our research in software product line engineering. The graphical security models are based on attributed attack-defense diagrams to capture the structure and properties of vulnerabilities, defenses and countermeasures--with notable similarities to feature diagrams--and on probabilistic models of attack behavior, capable of capturing resource constraints and attack effectiveness. In this paper, we provide an overview of the framework that is described in full technical detail in twin papers, which present the formal syntax and semantics of the domain-specific language and showcase the associated tool with advanced IDE support for performing analyses based on statistical model checking. The properties of interest range from average cost and success probability of attacks to the effectiveness of defenses and countermeasures. Here we illustrate the capabilities of the DSL and the tool by applying them to an example scenario from the security domain. This shows how techniques from variability modeling can be applied to security. We conclude with a vision and roadmap for future research.Source: VaMoS'20 - 14th International Working Conference on Variability Modelling of Software-Intensive Systems, pp. 11:1–11:9, Magdeburg, Germany, 5-7 February 2020
DOI: 10.1145/3377024.3377041
Project(s): CyberSec4Europe via OpenAIRE

See at: Unknown Repository Open Access | Archivio della ricerca della Scuola Superiore Sant'Anna Open Access | ISTI Repository Open Access | Online Research Database In Technology Open Access | Unknown Repository Restricted | Unknown Repository Restricted | dl.acm.org Restricted | Unknown Repository Restricted | CNR ExploRA Restricted


2020 Conference object Open Access OPEN

Family-based SPL model checking using parity games with variability
Ter Beek M. H., Van Loo S., De Vink E. P., Willemse T. A. C.
Family-based SPL model checking concerns the simultaneous verification of multiple product models, aiming to improve on enumerative product-based verification, by capitalising on the common features and behaviour of products in a software product line (SPL), typically modelled as a featured transition system (FTS). We propose efficient family-based SPL model checking of modal mu-calculus formulae on FTSs based on variability parity games, which extend parity games with conditional edges labelled with feature configurations, by reducing the SPL model checking problem for the modal mu-calculus on FTSs to the variability parity game solving problem, based on an encoding of FTSs as variability parity games. We validate our contribution by experiments on SPL benchmark models, which demonstrate that a novel family-based algorithm to collectively solve variability parity games, using symbolic representations of the configuration sets, outperforms the product-based method of solving the standard parity games obtained by projection with classical algorithms.Source: FASE 2020 - International Conference on Fundamental Approaches to Software Engineering, pp. 245–265, Dublin, Ireland, 25-30/04/2020
DOI: 10.1007/978-3-030-45234-6_12

See at: Europe PubMed Central Open Access | link.springer.com Open Access | Unknown Repository Open Access | ISTI Repository Open Access | CNR ExploRA Open Access | Unknown Repository Restricted | Unknown Repository Restricted | Unknown Repository Restricted | Unknown Repository Restricted | Unknown Repository Restricted


2020 Article Open Access OPEN

Synthesis of orchestrations and choreographies: bridging the gap between supervisory control and coordination of services
Basile D., Ter Beek M. H., Pugliese R.
We present a number of contributions to bridging the gap between supervisory control theory and coordination of services in order to explore the frontiers between coordination and control systems. Firstly, we modify the classical synthesis algorithm from supervisory control theory for obtaining the so-called most permissive controller in order to synthesise orchestrations and choreographies of service contracts formalised as contract automata. The key ingredient to make this possible is a novel notion of controllability. Then, we present an abstract parametric synthesis algorithm and show that it generalises the classical synthesis as well as the orchestration and choreography syntheses. Finally, through the novel abstract synthesis, we show that the concrete syntheses are in a refinement order. A running example from the service domain illustrates our contributions.Source: Logical Methods in Computer Science 16 (2020). doi:10.23638/LMCS-16(2:9)2020
DOI: 10.23638/LMCS-16(2:9)2020
DOI: 10.23638/lmcs-16(2:9)2020

See at: arXiv.org e-Print Archive Open Access | lmcs.episciences.org Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2020 Conference object Open Access OPEN

Team Automata@Work: On Safe Communication
Ter Beek M. H., Hennicker R., Kleijn J.
We study requirements for safe communication in systems of reactive components in which components communicate via synchronized execution of common actions. These systems are modelled in the framework of team automata in which any number of components can participate--as a sender or as a receiver--in the execution of a communication action. Moreover, there is no fixed synchronisation policy as these policies in general depend on the application. In this short paper, we reconsider the concept of safe communication in terms of reception and responsiveness requirements, originally defined for synchronisation policies determined by a synchronisation type. Illustrated by a motivating example, we propose three extensions. First, compliance, i.e. satisfaction of communication requirements, does not have to be immediate. Second, the synchronisation type (and hence the communication requirements) no longer has to be uniform, but can be specified per action. Third, we introduce final states to be able to distinguish between possible and guaranteed executions of actions.Source: 22nd IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION'20), pp. 77–85, Valletta, Malta, 15-19 June 2020
DOI: 10.1007/978-3-030-50029-0_5

See at: Europe PubMed Central Open Access | Unknown Repository Open Access | ISTI Repository Open Access | Unknown Repository Restricted | Unknown Repository Restricted | Unknown Repository Restricted | Unknown Repository Restricted | CNR ExploRA Restricted | Unknown Repository Restricted | Unknown Repository Restricted


2020 Conference object Open Access OPEN

Strategy Synthesis for Autonomous Driving in a Moving Block Railway System with Uppaal Stratego
Basile D., Ter Beek M. H., Legay A.
Moving block railway systems are the next generation signalling systems currently under development as part of the Shift2Rail European initiative, including autonomous driving technologies. In this paper, we model a suitable abstraction of a moving block signalling system with autonomous driving as a stochastic priced timed game. We then synthesise safe and optimal driving strategies for the model by applying advanced techniques that combine statistical model checking with reinforcement learning as provided by Uppaal Stratego. Hence, we show the applicability of Uppaal Stratego in this concrete case study.Source: 40th IFIP WG 6.1 International Conference on FORmal TEchniques for Distributed Objects, Components, and Systems (FORTE'20), pp. 3–21, Valletta, Malta, 15-19/06/2020
DOI: 10.1007/978-3-030-50086-3_1
Project(s): 4SECURAIL via OpenAIRE

See at: Europe PubMed Central Open Access | Unknown Repository Open Access | ISTI Repository Open Access | Unknown Repository Restricted | Unknown Repository Restricted | Unknown Repository Restricted | Unknown Repository Restricted | Unknown Repository Restricted | CNR ExploRA Restricted | Unknown Repository Restricted


2020 Conference object Open Access OPEN

Comparing formal tools for system design: a judgment study
Ferrari A, Mazzantif., Basile D., Ter Beek M. H., Fantechi A.
Formal methods and tools have a long history of successful applications in the design of safety-critical railway products. However, most of the experiences focused on the application of a single method at once, and little work has been performed to compare the applicability of the different available frameworks to the railway context. As a result, companies willing to introduce formal methods in their development process have little guidance on the selection of tools that couldfi t their needs. To address this goal, this paper presents a comparison between 9 different formal tools, namely Atelier B, CADP, FDR4, NuSMV, ProB, Simulink, SPIN, UMC, and UPPAAL SMC. We performed a judgment study, involving 17 experts with experience in formal methods applied to railways. In the study, part of the experts were required to model a railway signaling problem (a moving-block train distancing system) with the different tools, and to provide feedback on their experience. The information produced was then synthesized, and the results were validated by the remaining experts. Based on the outcome of this process, we provide a synthesis that describes when to use a certain tool, and what are the problems that may be faced by modelers. Our experience shows that the different tools serve different purposes, and multiple formal methods are required to fully cover the needs of the railway system design process.Source: ICSE'20 - 42nd International Conference on Software Engineering, pp. 62–74, Seoul, Republic of Korea, 27/6/2020-19/7/2020
DOI: 10.1145/3377811.3380373
Project(s): 4SECURAIL via OpenAIRE, ASTRail via OpenAIRE

See at: Unknown Repository Open Access | ISTI Repository Open Access | 2020.icse-conferences.org Restricted | Unknown Repository Restricted | Unknown Repository Restricted | Unknown Repository Restricted | Unknown Repository Restricted | CNR ExploRA Restricted


2020 Book Open Access OPEN

Formal Methods for Industrial Critical Systems - Proceedings of the 25th International Conference on Formal Methods for Industrial Critical Systems (FMICS'20)
Ter Beek M. H., Ni?kovi? D.
This book constitutes the proceedings of the 25th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2020, which was held during September 2-3, 2020. The conference was planned to take place in Vienna, Austria. Due to the COVID-19 pandemic it changed to a virtual event. The 11 full papers presented in this volume were carefully reviewed and selected from 26 submissions. The papers are organized in topical sections as follows: Quantitative Analysis and Cyber-Physical Systems, Formal Verification of Industrial Systems, Temporal Logic and Model Checking. The book also contains a lengthy report on a Formal Methods Survey conducted on occasion of the 25th edition of the conference.

See at: link.springer.com Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2020 Conference object Open Access OPEN

The 2020 Expert Survey on Formal Methods
Garavel H., Ter Beek M. H., Van De Pol J.
Organised to celebrate the 25th anniversary of the FMICS international conference, the present survey addresses 30 questions on the past, present, and future of formal methods in research, industry, and education. Not less than 130 high-profile experts in formal methods (among whom three Turing award winners and many recipients of other prizes and distinctions) accepted to participate in this survey. We analyse their answers and comments, and present a collection of 111 position statements provided by these experts. The survey is both an exercise in collective thinking and a family picture of key actors in formal methods.Source: 25th International Conference on Formal Methods for Industrial Critical Systems (FMICS'20), pp. 3–69, Vienna, Austria (online), 2-3/9/2020
DOI: 10.1007/978-3-030-58298-2_1

See at: Mémoires en Sciences de l'Information et de la Communication Open Access | Mémoires en Sciences de l'Information et de la Communication Open Access | Mémoires en Sciences de l'Information et de la Communication Open Access | Unknown Repository Open Access | ISTI Repository Open Access | PURE Aarhus University Open Access | Unknown Repository Restricted | Unknown Repository Restricted | Unknown Repository Restricted | Unknown Repository Restricted | link.springer.com Restricted | Unknown Repository Restricted | CNR ExploRA Restricted


2020 Article Open Access OPEN

Preface to Special issue dedicated to Jetty Kleijn on the occasion of her 65th birthday
Ter Beek M. H., Koutny M., Rozenberg G.
Source: Fundamenta informaticae 175 (2020): v–viii. doi:10.3233/FI-2020-1945
DOI: 10.3233/FI-2020-1945

See at: content.iospress.com Open Access | CNR ExploRA Open Access


2020 Conference object Open Access OPEN

Tackling the Equivalent Mutant Problem in Real-Time Systems: The 12 Commandments of Model-Based Mutation Testing
Basile D., Ter Beek M. H., Cordy M., Legay A.
Mutation testing can effectively drive test generation to reveal faults in software systems. However, it faces a typical efficiency issue as it can produce many mutants that are equivalent to the original system, making it impossible to generate test cases. We consider this problem when model-based mutation testing is applied to real-time system product lines, represented as timed automata. We define novel, time-specific mutation operators and formulate the equivalent mutant problem in the frame of timed refinement relations. Further, we study in which cases a mutation yields an equivalent mutant. Our theoretical results provide guidance to system engineers, allowing them to eliminate mutations from which no test case can be produced. Our evaluation, based on a proof-of-concept tool and an industrial case from the automotive domain, confirms the validity of our theory and demonstrates that our approach can eliminate many of the equivalent mutants (88% in our case study).Source: Proceedings of the 24th International Systems and Software Product Line Conference (SPLC'20), pp. 252–262, Montréal, Québec, Canada, 19-23/10/2020
DOI: 10.1145/3382025.3414966

See at: ISTI Repository Open Access | Unknown Repository Restricted | Unknown Repository Restricted | dl.acm.org Restricted | Unknown Repository Restricted | CNR ExploRA Restricted


2020 Conference object Open Access OPEN

Designing a demonstrator of formal methods for railways infrastructure managers
Basile D., Ter Beek M. H., Fantechi A., Ferrari A., Gnesi S., Masullo L., Mazzanti F., Piattino A., Trentini D.
The Shift2Rail Innovation Programme (IP) is focussing on innovative technologies to enhance the overall railway market segments. Formal methods and standard interfaces have been identified as two key concepts to reduce time-to-market and costs, while ensuring safety, interoperability and standardisation. However, the decision to start using formal methods is still deemed too risky. Demonstrating technical and commercial benefits of both formal methods and standard interfaces is necessary to address the obstacles of learning curve and lack of clear cost/benefit analysis that are hindering their adoption, and this is the goal of the 4SECURail project, recently funded by the Shift2Rail IP. In this paper, we provide the reasoning and the rationale for designing the formal methods demonstrator for the 4SECURail project. The design concerns two important issues that have been analysed: (i) the usefulness of formal methods from the point of view of the infrastructure managers, (ii) the adoption of a semi-formal SysML notation within our formal methods demonstrator process.Source: ISoLA'20 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Applications, pp. 467–485, Rhodes, Greece, 20-30 October, 2020
DOI: 10.1007/978-3-030-61467-6_30
Project(s): 4SECURAIL via OpenAIRE

See at: ISTI Repository Open Access | ISTI Repository Open Access | link.springer.com Restricted | Unknown Repository Restricted | CNR ExploRA Restricted


2020 Conference object Restricted

X-by-construction: correctness meets probability
Ter Beek M. H., Cleophas L., Legay A., Schaefer I., Watson B. W.
In recent years, researchers have started to investigate X-by-Construction (XbC) as a refinement approach to engineer systems that by-construction satisfy certain non-functional properties, beyond correctness as considered by the more traditional Correctness-by-Construction (CbC). In line with increasing attention for fault-tolerance and the use of machine-learning techniques in modern software systems, in which even correctness is hard to establish, this track brings together researchers and practitioners that are interested in XbC in particular in the setting of probabilistic properties.Source: ISoLA 2020 - 9th International Symposium on Leveraging Applications of Formal Methods, pp. 211–215, Rhodes, Greece, 20-30 October, 2020
DOI: 10.1007/978-3-030-61362-4_11

See at: link.springer.com Restricted | Unknown Repository Restricted | CNR ExploRA Restricted


2020 Conference object Open Access OPEN

30 years of simulation-based quantitative analysis tools: a comparison experiment between Möbius and Uppaal SMC
Basile D., Ter Beek M. H., Di Giandomenico F., Fantechi A., Gnesi S., Spagnolo G. O.
We provide a brief comparison of the modelling and analysis capabilities of two different formalisms and their associated simulation-based tools, acquired from experimenting with these methods and tools on one specific case study. The case study is a cyber-physical system from an industrial railway project, namely a railroad switch heater, and the quantitative properties concern energy consumption and reliability. We modelled and analysed the case study with stochastic activity networks and Möbius on the one hand and with stochastic hybrid automata and Uppaal SMC on the other hand. We give an overview of the performed experiments and highlight specific features of the two methodologies. This yields some pointers for future research and improvements.Source: ISoLA 2020 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, pp. 368–384, Rhodes, Greece, 20-30/10/2020
DOI: 10.1007/978-3-030-61362-4_21

See at: ISTI Repository Open Access | link.springer.com Restricted | Unknown Repository Restricted | CNR ExploRA Restricted


2020 Conference object Open Access OPEN

Compositionality of Safe Communication in Systems of Team Automata
Ter Beek M. H., Hennicker R., Kleijn J.
We study guarantees for safe communication in systems of systems composed of reactive components that communicate through synchronised execution of common actions. Systems are modelled as (extended) team automata, in which, in principle, any number of component automata can participate in the execution of a communicating action, either as a sender or as a receiver. We extend team automata with synchronisation type specifications, which determine specific synchronisation policies fine-tuned for particular application domains. On the other hand, synchronisation type specifications generate communication requirements for receptiveness and responsiveness. We propose a new, liberal version of requirement satisfaction which allows teams to execute arbitrary intermediate actions before being ready for the required communication, which is important in practice. Then we turn to the composition of systems and show that composition behaves well with respect to synchronisation type specifications. As a central result, we investigate criteria that ensure the preservation of local communication properties when (extended) team automata are composed. This is particularly challenging in the context of weak requirement satisfaction.Source: 17th International Colloquium on Theoretical Aspects of Computing (ICTAC'20), pp. 200–220, Macau, China, 30/11/2020-04/12/2020
DOI: 10.1007/978-3-030-64276-1_11
DOI: 10.5281/zenodo.4050293

See at: ISTI Repository Open Access | ZENODO Open Access | link.springer.com Restricted | Unknown Repository Restricted | CNR ExploRA Restricted


2020 Article Open Access OPEN

25th International Conference on Formal Methods for Industrial Critical Systems
Ter Beek M.
Source: ERCIM news 123 (2020): 5–5.

See at: ercim-news.ercim.eu Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2019 Article Open Access OPEN

On the expressiveness of modal transition systems with variability constraints
Ter Beek M., Damiani F., Gnesi S., Mazzanti F., Paolini L.
We demonstrate that modal transition systems with variability constraints are equally expressive as featured transition systems, by defining a transformation of the latter into the former, a transformation of the former into the latter, and proving the soundness and completeness of both transformations. Modal transition systems and featured transition systems are widely recognised as fundamental behavioural models for software product lines and our results thus contribute to the expressiveness hierarchy of such basic models studied in other papers published in this journal.Source: Science of computer programming (Print) 169 (2019): 1–17. doi:10.1016/j.scico.2018.09.006
DOI: 10.1016/j.scico.2018.09.006

See at: ISTI Repository Open Access | Science of Computer Programming Restricted | Science of Computer Programming Restricted | Science of Computer Programming Restricted | Science of Computer Programming Restricted | CNR ExploRA Restricted | Science of Computer Programming Restricted