2005
Journal article
Restricted
A formal security analysis of an OSA/Parlay authentication interface
Corin R, Di Caprio G, Etalle S, Gnesi S, Lenzini G, Moiso C
We report on an experience in analyzing the security of the Trust and Security Management (TSM) protocol, an authentication procedure within the OSA/Parlay Application Program Interfaces (APIs) of the Open Service Access and Parlay Group. The experience has been conducted jointly by research institutes experienced in security and industry experts in telecommunication networking. OSA/Parlay APIs are designed to enable the creation of telecommunication applications outside the traditional network space and business model. Network operators consider the OSA/Parlay a promising architecture to stimulate the development of web service applications by third party providers, which may not necessarily be experts in telecommunication and security. The TSM protocol is executed by the gateways to OSA/Parlay networks; its role is to authenticate client applications trying to access the interfaces of some object representing an offered network capability. For this reason, potential security flaws in the TSM authentication strategy can cause the unauthorized use of the network, with evident damages to the operator and the quality of services. We report a rigorous formal analysis of the TSM specification, which is originally given in UML. Furthermore, we illustrate our design choices to obtain the formal model, describe the tool-aided verification and finally expose the security flaws discovered.
Corin R, Di Caprio G, Etalle S, Gnesi S, Lenzini G, Moiso C
We report on an experience in analyzing the security of the Trust and Security Management (TSM) protocol, an authentication procedure within the OSA/Parlay Application Program Interfaces (APIs) of the Open Service Access and Parlay Group. The experience has been conducted jointly by research institutes experienced in security and industry experts in telecommunication networking. OSA/Parlay APIs are designed to enable the creation of telecommunication applications outside the traditional network space and business model. Network operators consider the OSA/Parlay a promising architecture to stimulate the development of web service applications by third party providers, which may not necessarily be experts in telecommunication and security. The TSM protocol is executed by the gateways to OSA/Parlay networks; its role is to authenticate client applications trying to access the interfaces of some object representing an offered network capability. For this reason, potential security flaws in the TSM authentication strategy can cause the unauthorized use of the network, with evident damages to the operator and the quality of services. We report a rigorous formal analysis of the TSM specification, which is originally given in UML. Furthermore, we illustrate our design choices to obtain the formal model, describe the tool-aided verification and finally expose the security flaws discovered.
See at:
CNR IRIS 
| CNR IRIS | link.springer.com
2006
Journal article
Restricted
Achieving fault tolerance by a formally validated interaction policy
Fantechi A, Gnesi S, Semini L
This paper presents the rigorous validation of an integrity policy by means of the application of formal methods and related support tools for its specification and verification. The protocol which carries out the integrity policy is formally specified and formally validated, exploiting model-checking. Specific interaction patterns, which subsume the most complex interaction schemata, are considered and temporal logic formulae expressing the non-violation of integrity rules are checked on them.
Fantechi A, Gnesi S, Semini L
This paper presents the rigorous validation of an integrity policy by means of the application of formal methods and related support tools for its specification and verification. The protocol which carries out the integrity policy is formally specified and formally validated, exploiting model-checking. Specific interaction patterns, which subsume the most complex interaction schemata, are considered and temporal logic formulae expressing the non-violation of integrity rules are checked on them.
2003
Journal article
Restricted
A model-checking verification environment for mobile processes
Ferrari Gl, Gnesi S, Montanari U, Pistore M
This article presents a semantic-based environment for reasoning about the behavior of mobile systems. The verification environment, called HAL, exploits a novel automata-like model that allows finite-state verification of systems specified in the ?-calculus. The HAL system is able to interface with several efficient toolkits (e.g. model-checkers) to determine whether or not certain properties hold for a given specification. We report experimental results on some case studies.Source: ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, vol. 12, pp. 440-473
Ferrari Gl, Gnesi S, Montanari U, Pistore M
This article presents a semantic-based environment for reasoning about the behavior of mobile systems. The verification environment, called HAL, exploits a novel automata-like model that allows finite-state verification of systems specified in the ?-calculus. The HAL system is able to interface with several efficient toolkits (e.g. model-checkers) to determine whether or not certain properties hold for a given specification. We report experimental results on some case studies.Source: ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, vol. 12, pp. 440-473
2003
Book
Open Access
FME 2003: Formal Methods
Araki K, Gnesi S, Mandrioli D
This volume contains the proceedings of FM 2003, the 12th International Formal Methods Europe Symposium which was held in Pisa, Italy on September 8 14, 2003. Formal Methods Europe (FME, www.fmeurope.org) is an independent association which aims to stimulate the use of and research on formal methods for system development. FME conferences began with a VDM Europe symposium in 1987. Since then, the meetings have grown and have been held about once every 18 months. Throughout the years the symposia have been notably successful in bringing together researchers, tool developers, vendors, and users, both from academia and from industry. Unlike previous symposia in the series, FM 2003 was not given a speci c theme. Rather, its main goal could be synthesized as widening the scope. Indeed, the organizers aimed at enlarging the audience and impact of the symposium along several directions. Dropping the su x E from the title of the conference re ects the wish to welcome participation and contribution from every country; also, contributions from outside the traditional Formal Methods community were solicited. The recent innovation of including an Industrial Day as an important part of the symposium shows the strong commitment to involve industrial people more and more within the Formal Methods community.
Araki K, Gnesi S, Mandrioli D
This volume contains the proceedings of FM 2003, the 12th International Formal Methods Europe Symposium which was held in Pisa, Italy on September 8 14, 2003. Formal Methods Europe (FME, www.fmeurope.org) is an independent association which aims to stimulate the use of and research on formal methods for system development. FME conferences began with a VDM Europe symposium in 1987. Since then, the meetings have grown and have been held about once every 18 months. Throughout the years the symposia have been notably successful in bringing together researchers, tool developers, vendors, and users, both from academia and from industry. Unlike previous symposia in the series, FM 2003 was not given a speci c theme. Rather, its main goal could be synthesized as widening the scope. Indeed, the organizers aimed at enlarging the audience and impact of the symposium along several directions. Dropping the su x E from the title of the conference re ects the wish to welcome participation and contribution from every country; also, contributions from outside the traditional Formal Methods community were solicited. The recent innovation of including an Industrial Day as an important part of the symposium shows the strong commitment to involve industrial people more and more within the Formal Methods community.
See at:
CNR IRIS 
| link.springer.com | CNR IRIS
2008
Journal article
Restricted
Graph-based design and analysis of dynamic software architectures
Bucchiarone A, Gnesi S, Bruni R, Lafuente A L, Hirsch D
We illustrate two ways to address the specification, modelling and analysis of dynamic software architectures using: i) ordinary typed graph transformation techniques implemented in Alloy; ii) a process algebraic presentation of graph transformation implemented inMaude. The two approaches are compared by showing how different aspects can be tackled, including representation issues, modelling phases, property specification and analysis.
Bucchiarone A, Gnesi S, Bruni R, Lafuente A L, Hirsch D
We illustrate two ways to address the specification, modelling and analysis of dynamic software architectures using: i) ordinary typed graph transformation techniques implemented in Alloy; ii) a process algebraic presentation of graph transformation implemented inMaude. The two approaches are compared by showing how different aspects can be tackled, including representation issues, modelling phases, property specification and analysis.
2008
Contribution to book
Restricted
Software engineering: Ugo Montanari's main contributions and introduction to the section
Gnesi S
Ugo Montanari began to work in software engineering related topics in the early eighties when he started to promote the use of formal techniques in industries. In that period Ugo established a strong cooperation mainly with Olivetti, that was for more than a decade a very active italian ICT company. Those were also the years when the first Progetto Finalizzato Informatica started and in this contextUgo chaired the P1 subproject, "IndustriaNazionale del settore: Architettura e Struttura dei Sistemi di Elaborazione" whose aims were: i) the development of a prototypical local network meant also to be used to develop software products for the public administration; ii) the realization of a prototypical micro processor with dependability, availability and reconfigurability characteristics to be employed for industrial automation; iii) the development of methods and software programs to be used as basis for the software production.
Gnesi S
Ugo Montanari began to work in software engineering related topics in the early eighties when he started to promote the use of formal techniques in industries. In that period Ugo established a strong cooperation mainly with Olivetti, that was for more than a decade a very active italian ICT company. Those were also the years when the first Progetto Finalizzato Informatica started and in this contextUgo chaired the P1 subproject, "IndustriaNazionale del settore: Architettura e Struttura dei Sistemi di Elaborazione" whose aims were: i) the development of a prototypical local network meant also to be used to develop software products for the public administration; ii) the realization of a prototypical micro processor with dependability, availability and reconfigurability characteristics to be employed for industrial automation; iii) the development of methods and software programs to be used as basis for the software production.
See at:
CNR IRIS | CNR IRIS | link.springer.com
2003
Journal article
Open Access
Model checking of embedded systems
Gnesi S
The integration of different dependability techniques is an open research question. We address problems that arise when attempting to combine fault tolerance mechanisms with formal methods and formal verification tools in the development of an embedded system.Source: ERCIM NEWS, vol. 52, pp. 37-38
Gnesi S
The integration of different dependability techniques is an open research question. We address problems that arise when attempting to combine fault tolerance mechanisms with formal methods and formal verification tools in the development of an embedded system.Source: ERCIM NEWS, vol. 52, pp. 37-38
See at:
CNR IRIS | www.ercim.org | CNR IRIS
2006
Journal article
Restricted
The industrialization of formal methods
Fitzgerald J S, Gnesi S, Mandrioli D
This special section contains papers based on work presented at the 12th International Symposium on Formal Methods (FM 2003) held at the CNR Research Campus in Pisa on 8-13 September 2003. The papers all focus on tools and techniques for cost-effective application of formal methods on the industrial scale. The papers discuss a range of approaches, including the development of domain-specific and general-purpose techniques, and the construction of suites of cooperating but specialised tools. In spite of the diversity of approach, the papers share some themes, notably the levels of automation that are possible at appropriate levels of abstraction, and the incorporation of formal techniques within existing development paradigms. Although three papers cannot provide a comprehensive view, they do provide a useful 'snapshot' of dominant concerns in industrial-strength formal methods today.Source: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER (INTERNET), vol. 8 (issue 4-5), pp. 301-302
Fitzgerald J S, Gnesi S, Mandrioli D
This special section contains papers based on work presented at the 12th International Symposium on Formal Methods (FM 2003) held at the CNR Research Campus in Pisa on 8-13 September 2003. The papers all focus on tools and techniques for cost-effective application of formal methods on the industrial scale. The papers discuss a range of approaches, including the development of domain-specific and general-purpose techniques, and the construction of suites of cooperating but specialised tools. In spite of the diversity of approach, the papers share some themes, notably the levels of automation that are possible at appropriate levels of abstraction, and the incorporation of formal techniques within existing development paradigms. Although three papers cannot provide a comprehensive view, they do provide a useful 'snapshot' of dominant concerns in industrial-strength formal methods today.Source: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER (INTERNET), vol. 8 (issue 4-5), pp. 301-302
2003
Journal article
Restricted
Formal specification and verification of complex systems
Gnesi S
The application of formal methods in the rigorous de nition and analysis of the functionality and the behaviour of a system, promises the ability of showing that the system is correct. Given such a promise, that is already out since several years, it is astonishing to see how little formal methods are actually used in the safety critical system industry, though the use of formal methods is increasingly required by the international standards and guidelines for the development of complex systems.Source: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, vol. 80, pp. 1-5
Gnesi S
The application of formal methods in the rigorous de nition and analysis of the functionality and the behaviour of a system, promises the ability of showing that the system is correct. Given such a promise, that is already out since several years, it is astonishing to see how little formal methods are actually used in the safety critical system industry, though the use of formal methods is increasingly required by the international standards and guidelines for the development of complex systems.Source: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, vol. 80, pp. 1-5
See at:
CNR IRIS | CNR IRIS | www.elsevier.nl
2008
Journal article
Restricted
Modelling dynamic software architectures using typed graph grammars
Bruni R, Bucchiarone A, Gnesi S, Melgratti H
Several recent research efforts have focused on the dynamic aspects of software architectures providing suitable models and techniques for handling the run-time modification of the structure of a system. A large number of heterogeneous proposals for addressing dynamic architectures at many different levels of abstraction have been provided, such as programmable, ad-hoc, self-healing and self-repairing among others. It is then important to have a clear picture of the relations among these proposals by formulating them into a uniform framework and contrasting the different verification aspects that can be reasonably addressed by each proposal. Our work is a contribution in this line. In particular, we map several notions of dynamicity into the same formal framework in order to distill the similarities and differences among them. As a result we explain different styles of architectural dynamisms in term of graph grammars and get some better insights on the kinds of formal properties that can be naturally associated to such different specification styles. We take a simple automotive scenario as a running example to illustrate main ideas.Source: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, vol. 213 (issue 1), pp. 39-53
Bruni R, Bucchiarone A, Gnesi S, Melgratti H
Several recent research efforts have focused on the dynamic aspects of software architectures providing suitable models and techniques for handling the run-time modification of the structure of a system. A large number of heterogeneous proposals for addressing dynamic architectures at many different levels of abstraction have been provided, such as programmable, ad-hoc, self-healing and self-repairing among others. It is then important to have a clear picture of the relations among these proposals by formulating them into a uniform framework and contrasting the different verification aspects that can be reasonably addressed by each proposal. Our work is a contribution in this line. In particular, we map several notions of dynamicity into the same formal framework in order to distill the similarities and differences among them. As a result we explain different styles of architectural dynamisms in term of graph grammars and get some better insights on the kinds of formal properties that can be naturally associated to such different specification styles. We take a simple automotive scenario as a running example to illustrate main ideas.Source: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, vol. 213 (issue 1), pp. 39-53
See at:
CNR IRIS | CNR IRIS | www.sciencedirect.com
2009
Journal article
Restricted
A graph-based design framework for global computing systems
Bucchiarone A, Gnesi S, Dennis G
We present a framework for designing and analyzing Global Computing Systems using Dynamic Software Architectures. The framework, called TGGA, integrates typed graph grammars and the Alloy modeling language to specify Programmed Dynamic Software Architectures that represent systems that evolve their topology at runtime. We demonstrate the benefits of the framework by applying it to the study of an Automotive Software System.Source: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, vol. 236, pp. 117-130
Bucchiarone A, Gnesi S, Dennis G
We present a framework for designing and analyzing Global Computing Systems using Dynamic Software Architectures. The framework, called TGGA, integrates typed graph grammars and the Alloy modeling language to specify Programmed Dynamic Software Architectures that represent systems that evolve their topology at runtime. We demonstrate the benefits of the framework by applying it to the study of an Automotive Software System.Source: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, vol. 236, pp. 117-130
See at:
CNR IRIS | CNR IRIS | www.sciencedirect.com
2004
Conference article
Restricted
Security analysis of parlay/OSA framework
Corin R, Di Caprio G, Etalle S, Gnesi S, Lenzini G, Moiso C
This paper reports an analysis of the security of the Trust and Security Management (TSM) protocol, an authentication protocol which is part of the Parlay/OSA Application Program Interfaces (APIs). Parlay/OSA APIs allow third party service providers to develop new services that can access, in a controlled and secure way, the network capabilities offered by the network operator. The role of the TSM protocol, run by network gateways, is to authenticate the client applications trying to access and to use the services offered. For this reason, potential security flaws in the authentication protocol can lead to unauthorized use of the network with evident damages to the operator and to the quality of services. This paper shows how a rigorous formal analysis of the TSM protocol allowed us to discover serious weaknesses in the model describing its authentication procedure. The paper reports on the design activity of the formal model, the toolaided verification we carried out and the security flaws we discovered. This allows us to discuss how the security of the TSM protocol can be generally improved.
Corin R, Di Caprio G, Etalle S, Gnesi S, Lenzini G, Moiso C
This paper reports an analysis of the security of the Trust and Security Management (TSM) protocol, an authentication protocol which is part of the Parlay/OSA Application Program Interfaces (APIs). Parlay/OSA APIs allow third party service providers to develop new services that can access, in a controlled and secure way, the network capabilities offered by the network operator. The role of the TSM protocol, run by network gateways, is to authenticate the client applications trying to access and to use the services offered. For this reason, potential security flaws in the authentication protocol can lead to unauthorized use of the network with evident damages to the operator and to the quality of services. This paper shows how a rigorous formal analysis of the TSM protocol allowed us to discover serious weaknesses in the model describing its authentication procedure. The paper reports on the design activity of the formal model, the toolaided verification we carried out and the security flaws we discovered. This allows us to discuss how the security of the TSM protocol can be generally improved.
2005
Conference article
Restricted
Quality analysis of NL requirements: an industrial case study
Bucchiarone A, Gnesi S
Nowadays common practice indicates that the Requirement Engineering (RE) process critically influences the success of the system development life cycle. Several commercial tools allow to classify, archive and manage requirements and then to print out reports and requirement documents. QuARS (Quality Analyzer for Requirements Specifications) is an automatic analyzer of such requirement documents, developed by ISTI - CNR, that can be adopted to evaluate the document quality by linguistic point of view. In this paper is presented how a requirement management tool, an automatic document generator and QuARS can be integrated to define an RE automation support. The case study investigates and highlights the efficacy and the role of such proposed support in the Siemens C.N.X. development process.
Bucchiarone A, Gnesi S
Nowadays common practice indicates that the Requirement Engineering (RE) process critically influences the success of the system development life cycle. Several commercial tools allow to classify, archive and manage requirements and then to print out reports and requirement documents. QuARS (Quality Analyzer for Requirements Specifications) is an automatic analyzer of such requirement documents, developed by ISTI - CNR, that can be adopted to evaluate the document quality by linguistic point of view. In this paper is presented how a requirement management tool, an automatic document generator and QuARS can be integrated to define an RE automation support. The case study investigates and highlights the efficacy and the role of such proposed support in the Siemens C.N.X. development process.
2006
Conference article
Restricted
A survey on services composition languages and models
Bucchiarone A, Gnesi S
Composition of services has received much interest to support business-to-business (B2B) or enterprise applications integration. On one side, the business world has developed a number of XML-based standards to formalize the specification of Web services, their composition and execution. On the other side, the Semantic Web community focuses on reasoning about web resources by explicitly declaring theirpreconditions and effects with terms precisely defined in ontologies. So far, both approaches have been developed rather independently from each other. In this paper the major languages, namely BPEL4WS, BPML, WSCI, WS-CDL and DAML-S, are compared with reference to the requirements identified and finally the trend of Services composition is discussed.
Bucchiarone A, Gnesi S
Composition of services has received much interest to support business-to-business (B2B) or enterprise applications integration. On one side, the business world has developed a number of XML-based standards to formalize the specification of Web services, their composition and execution. On the other side, the Semantic Web community focuses on reasoning about web resources by explicitly declaring theirpreconditions and effects with terms precisely defined in ontologies. So far, both approaches have been developed rather independently from each other. In this paper the major languages, namely BPEL4WS, BPML, WSCI, WS-CDL and DAML-S, are compared with reference to the requirements identified and finally the trend of Services composition is discussed.
2007
Conference article
Restricted
Automatic Instantiation for Railway Interlocking Systems
Banci M, Gnesi S
Real-life systems can be conveniently modeled by the replication and interconnection of simple components of few types: different configurations of the same system may vary just for the number of components and for the topology of their interconnections. In industrial practice of formal modeling the tedious work of manual instantiation has to be automated, which allows to produce at low cost new configurations of the same product. We propose a methodology to build formal statechart models of topologically distributed systems by instantiating generic components
Banci M, Gnesi S
Real-life systems can be conveniently modeled by the replication and interconnection of simple components of few types: different configurations of the same system may vary just for the number of components and for the topology of their interconnections. In industrial practice of formal modeling the tedious work of manual instantiation has to be automated, which allows to produce at low cost new configurations of the same product. We propose a methodology to build formal statechart models of topologically distributed systems by instantiating generic components
2002
Contribution to conference
Metadata Only Access
See at:
CNR IRIS
2002
Contribution to conference
Metadata Only Access
See at:
CNR IRIS
2004
Other
Open Access
The role of formal methods in developing a distribuited railwai interlocking system
Banci M, Fantechi A, Gnesi S
The development of computer controlled Railway Interlocking Systems (RIS) has seen an increasing interest in the use of Formal Methods, due to their ability to precisely specify the logical rules that guarantee the safe establishment of routes for trains through a railway yard. Recently, a trend has emerged about the use of statecharts as a standard formalism to produce precise specifications of RIS. This paper describes an experience in modelling a railway interlocking system using statecharts. Our study has addressed the problem from a 'geographic', distributed, point of view: that is, our model is composed by models of single physical entities (points, signals, etc..) that collectively implement the interlocking rules, without any centralized database of rules, which is on the other hand a typical way of implementing such a system (what we call 'functional' approach). We show how a distributed model of this kind may be used to develop a distributed implementation, that employs physically distributed controllers communicating through a 'safe' field bus. Ensuring safety of this kind of RIS is entirely based on formal verification.
Banci M, Fantechi A, Gnesi S
The development of computer controlled Railway Interlocking Systems (RIS) has seen an increasing interest in the use of Formal Methods, due to their ability to precisely specify the logical rules that guarantee the safe establishment of routes for trains through a railway yard. Recently, a trend has emerged about the use of statecharts as a standard formalism to produce precise specifications of RIS. This paper describes an experience in modelling a railway interlocking system using statecharts. Our study has addressed the problem from a 'geographic', distributed, point of view: that is, our model is composed by models of single physical entities (points, signals, etc..) that collectively implement the interlocking rules, without any centralized database of rules, which is on the other hand a typical way of implementing such a system (what we call 'functional' approach). We show how a distributed model of this kind may be used to develop a distributed implementation, that employs physically distributed controllers communicating through a 'safe' field bus. Ensuring safety of this kind of RIS is entirely based on formal verification.
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2010
Book
Restricted
Preface of SEFM 2010
Fiadeiro J, Gnesi S, Maggiolo Schettini A
This volume contains the proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2010) held on 13-18 September 2010 in Pisa, Italy, hosted by the Istituto di Scienza e Tecnologie dell'Informazione A. Faedo of the Consiglio Nazionale delle Ricerche (ISTI-CNR).
Fiadeiro J, Gnesi S, Maggiolo Schettini A
This volume contains the proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2010) held on 13-18 September 2010 in Pisa, Italy, hosted by the Istituto di Scienza e Tecnologie dell'Informazione A. Faedo of the Consiglio Nazionale delle Ricerche (ISTI-CNR).
See at:
CNR IRIS | ieeexplore.ieee.org | CNR IRIS
2003
Book
Open Access
Special issue on the Fifth International Workshop of the ERCIM Working Group on Formal Methods for Industrial Critical Systems
Garavel H, Gnesi S, Schieferdeckerc I
The purpose of this special issue of the International Journal Science in Computer Programming is to present a selection of papers from the Proceedings of the 5th ERCIM International Workshop on Formal Methods for Industrial Critical Systems (FMICS), which took place in Berlin in March 2000. FMICS is the ERCIM Working Group on Formal Methods for Industrial Critical Systems. Launched in 1996 by Diego Latella and Stefania Gnesi (CNR Pisa), the FMICS working group is currently chaired by Hubert Garavel (INRIA Rhone-Alpes).Source: SCIENCE OF COMPUTER PROGRAMMING, pp. 145-146
Garavel H, Gnesi S, Schieferdeckerc I
The purpose of this special issue of the International Journal Science in Computer Programming is to present a selection of papers from the Proceedings of the 5th ERCIM International Workshop on Formal Methods for Industrial Critical Systems (FMICS), which took place in Berlin in March 2000. FMICS is the ERCIM Working Group on Formal Methods for Industrial Critical Systems. Launched in 1996 by Diego Latella and Stefania Gnesi (CNR Pisa), the FMICS working group is currently chaired by Hubert Garavel (INRIA Rhone-Alpes).Source: SCIENCE OF COMPUTER PROGRAMMING, pp. 145-146
See at:
CNR IRIS | www.sciencedirect.com | CNR IRIS