2004
Journal article
Open Access
Composing event constraints in state-based specification
Bolognesi T.
Event-based process algebraic specification languages support an elegant specification technique by which system behaviours are described as compositions of constraints on event occurrences and event parameters. This paper investigates the possibility to export this specification paradigm to a state-based formalism, and discusses some deriving advantages in terms of verification.DOI: 10.1007/978-3-540-30232-2_2
Metrics:
Bolognesi T.
Event-based process algebraic specification languages support an elegant specification technique by which system behaviours are described as compositions of constraints on event occurrences and event parameters. This paper investigates the possibility to export this specification paradigm to a state-based formalism, and discusses some deriving advantages in terms of verification.DOI: 10.1007/978-3-540-30232-2_2
Metrics:
See at:
CNR IRIS 
| link.springer.com | www.springerlink.com | doi.org 
| CNR IRIS
2004
Journal article
Restricted
On competence in CD grammar systems
Ter Beek M, Csuhajvarju E, Holzer M, Vaszil G
We investigate the generative power of cooperating distributed grammar systems (CDGSs), if the cooperation protocol is based on the level of competence on the underlying sentential form. A component is said to be =k-competent (=k-competent, resp.) on a sentential form if it is able to rewrite exactly k (at most k, at least k, resp.) different nonterminals appearing in that string. In most cases CDGSs working according to the above described cooperation strategy turn out to give new characterizations of the language families based on random context conditions, namely random context (context-free) languages and the biologically motivated family of languages generated by ET0L systems with random context. Thus, the results presented in this paper can shed new light on some longstanding open problems in the theory of regulated rewriting.
Ter Beek M, Csuhajvarju E, Holzer M, Vaszil G
We investigate the generative power of cooperating distributed grammar systems (CDGSs), if the cooperation protocol is based on the level of competence on the underlying sentential form. A component is said to be =k-competent (=k-competent, resp.) on a sentential form if it is able to rewrite exactly k (at most k, at least k, resp.) different nonterminals appearing in that string. In most cases CDGSs working according to the above described cooperation strategy turn out to give new characterizations of the language families based on random context conditions, namely random context (context-free) languages and the biologically motivated family of languages generated by ET0L systems with random context. Thus, the results presented in this paper can shed new light on some longstanding open problems in the theory of regulated rewriting.
See at:
CNR IRIS | CNR IRIS | www.springerlink.com
2004
Journal article
Open Access
Teams of Pushdown Automata
Ter Beek Mh, Csuhajvarju E, Mitrana V
We introduce team pushdown automata (PDAs) as a theoretical framework capable of modelling various communication and cooperation strategies in complex, distributed systems. Team PDAs are obtained by augmenting distributed PDAs with the notion of team cooperation or, alternatively, by augmenting team automata with pushdown memory. In a team PDA, several PDAs work as a team on the input word placed on a common one-way input tape. At any moment in time one team of PDAs, each with the same symbol on top of its stack, is active: each PDA in the active team replaces the topmost symbol of its stack and changes state, while the current input symbol is read from the input tape by a common reading head. The teams are formed according to the team cooperation strategy of the team PDA and may vary from one moment to the other. Based on the notion of competence, we introduce a variety of team cooperation strategies. If all stacks are empty when the input word has been completely read, then this word is part of the language accepted by the team PDA. Here we focus on the accepting capacity of team PDA.Source: INTERNATIONAL JOURNAL OF COMPUTER MATHEMATICS, vol. 81 (issue 2), pp. 141-156
DOI: 10.1080/00207160310001650099
DOI: 10.1007/978-3-540-39866-0_32
Metrics:
Ter Beek Mh, Csuhajvarju E, Mitrana V
We introduce team pushdown automata (PDAs) as a theoretical framework capable of modelling various communication and cooperation strategies in complex, distributed systems. Team PDAs are obtained by augmenting distributed PDAs with the notion of team cooperation or, alternatively, by augmenting team automata with pushdown memory. In a team PDA, several PDAs work as a team on the input word placed on a common one-way input tape. At any moment in time one team of PDAs, each with the same symbol on top of its stack, is active: each PDA in the active team replaces the topmost symbol of its stack and changes state, while the current input symbol is read from the input tape by a common reading head. The teams are formed according to the team cooperation strategy of the team PDA and may vary from one moment to the other. Based on the notion of competence, we introduce a variety of team cooperation strategies. If all stacks are empty when the input word has been completely read, then this word is part of the language accepted by the team PDA. Here we focus on the accepting capacity of team PDA.Source: INTERNATIONAL JOURNAL OF COMPUTER MATHEMATICS, vol. 81 (issue 2), pp. 141-156
DOI: 10.1080/00207160310001650099
DOI: 10.1007/978-3-540-39866-0_32
Metrics:
See at:
International Journal of Computer Mathematics | doi.org | International Journal of Computer Mathematics | CNR IRIS | CNR IRIS | www.scopus.com | www.tandfonline.com
2005
Journal article
Restricted
A comparison between handwritten and automatic generation of C code from SDL using static analysis
Becucci M, Fantechi A, Giromini M, Spinicci E
The experience reported in this paper relates to an evaluation of the automatic generation of C code from the Specification and Description Language (SDL) specification of embedded applications. The evaluation has been carried out by comparing the automatically generated code with the manually implemented code, both compliant to the same SDL specification: this comparison is based on a selection of metrics measured on both codes by means of commercial static analysis tools. Notwithstanding the different structure of the two codes, we appropriately selected and aggregated the obtained results in order to use them as indicators of code size, control flow complexity and integration flow complexity. For a better comparison of the two codes, we have also introduced a novel complexity metric, which compares the control flow complexity with the integration flow of the two different software architectures. The aim of the paper is not merely to evaluate the code generator used, but rather to propose a set of techniques that can be used to conduct similar evaluations.Source: SOFTWARE, PRACTICE AND EXPERIENCE, vol. 35 (issue 14), pp. 1317-1347
DOI: 10.1002/spe.673
Metrics:
Becucci M, Fantechi A, Giromini M, Spinicci E
The experience reported in this paper relates to an evaluation of the automatic generation of C code from the Specification and Description Language (SDL) specification of embedded applications. The evaluation has been carried out by comparing the automatically generated code with the manually implemented code, both compliant to the same SDL specification: this comparison is based on a selection of metrics measured on both codes by means of commercial static analysis tools. Notwithstanding the different structure of the two codes, we appropriately selected and aggregated the obtained results in order to use them as indicators of code size, control flow complexity and integration flow complexity. For a better comparison of the two codes, we have also introduced a novel complexity metric, which compares the control flow complexity with the integration flow of the two different software architectures. The aim of the paper is not merely to evaluate the code generator used, but rather to propose a set of techniques that can be used to conduct similar evaluations.Source: SOFTWARE, PRACTICE AND EXPERIENCE, vol. 35 (issue 14), pp. 1317-1347
DOI: 10.1002/spe.673
Metrics:
See at:
Software Practice and Experience | CNR IRIS | CNR IRIS | onlinelibrary.wiley.com
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
2005
Journal article
Open Access
Modularity for teams of I/O automata
Ter Beek M. H., Kleijn J.
NoneSource: INFORMATION PROCESSING LETTERS, vol. 95 (issue 5), pp. 487-495
DOI: 10.1016/j.ipl.2005.05.012
Metrics:
Ter Beek M. H., Kleijn J.
NoneSource: INFORMATION PROCESSING LETTERS, vol. 95 (issue 5), pp. 487-495
DOI: 10.1016/j.ipl.2005.05.012
Metrics:
See at:
Information Processing Letters | Information Processing Letters | CNR IRIS | CNR IRIS | www.sciencedirect.com
2005
Journal article
Open Access
Synchronized shuffles
Ter Beek M. H., Martín-Vide C., Mitrana V.
We extend the basic shuffle on words and languages, a well-known operation in theoretical computer science, by introducing three synchronized shuffles. These synchronized shuffles have some relevance to molecular biology since they may be viewed as the formal representations of various forms of gene linkage during genome shuffling. More precisely, each synchronized shuffle preserves the genetic backbone of the organisms, as well as the linked genes, by requiring the synchronization of some predefined genes while all other genes are arbitrarily shuffled. As for their mathematical properties, we prove that in a trio the closure under shuffle is equivalent to the closure under any of the synchronized shuffles studied here. Finally, based on this result, we present an algorithm for deciding whether a given regular language is synchronized shuffle closed.Source: THEORETICAL COMPUTER SCIENCE, vol. 341 (issue 1-3), pp. 263-275
DOI: 10.1016/j.tcs.2005.04.007
Metrics:
Ter Beek M. H., Martín-Vide C., Mitrana V.
We extend the basic shuffle on words and languages, a well-known operation in theoretical computer science, by introducing three synchronized shuffles. These synchronized shuffles have some relevance to molecular biology since they may be viewed as the formal representations of various forms of gene linkage during genome shuffling. More precisely, each synchronized shuffle preserves the genetic backbone of the organisms, as well as the linked genes, by requiring the synchronization of some predefined genes while all other genes are arbitrarily shuffled. As for their mathematical properties, we prove that in a trio the closure under shuffle is equivalent to the closure under any of the synchronized shuffles studied here. Finally, based on this result, we present an algorithm for deciding whether a given regular language is synchronized shuffle closed.Source: THEORETICAL COMPUTER SCIENCE, vol. 341 (issue 1-3), pp. 263-275
DOI: 10.1016/j.tcs.2005.04.007
Metrics:
See at:
Theoretical Computer Science | CNR IRIS | CNR IRIS | www.sciencedirect.com
2006
Journal article
Unknown
A practical architecture-centric analysis process
Bucchiarone A., Muccini H., Pelliccione P.
When engineering complex and distributed software and hardware systems (increasingly used in many sectors, such as manufacturing, aerospace, transportation, communication, energy and health-care), dependability has became a must, since failures can have economics consequences and can also endanger human life. Software Architectures (SA) can help improving the overall system dependability, providing a system blueprint that can be validated and that can guide all phases of the system development. Even if much work has been done on this direction, three important topics require major investigation: how different analysis techniques can be integrated together, how results obtained with SA-based analysis can be related to requirements and coding, and how integrate new methodologies in the industrial software development life-cycle. In this paper we propose an architecture-centric analysis process which allows formal analysis driven by model-based architectural specifications. This analysis process satisfies the industrial requirements, since it is tool supported and based on semi-formal (UML-based) specifications.Source: Lecture notes in computer science (2006): 127–144.
Bucchiarone A., Muccini H., Pelliccione P.
When engineering complex and distributed software and hardware systems (increasingly used in many sectors, such as manufacturing, aerospace, transportation, communication, energy and health-care), dependability has became a must, since failures can have economics consequences and can also endanger human life. Software Architectures (SA) can help improving the overall system dependability, providing a system blueprint that can be validated and that can guide all phases of the system development. Even if much work has been done on this direction, three important topics require major investigation: how different analysis techniques can be integrated together, how results obtained with SA-based analysis can be related to requirements and coding, and how integrate new methodologies in the industrial software development life-cycle. In this paper we propose an architecture-centric analysis process which allows formal analysis driven by model-based architectural specifications. This analysis process satisfies the industrial requirements, since it is tool supported and based on semi-formal (UML-based) specifications.Source: Lecture notes in computer science (2006): 127–144.
See at: CNR ExploRA
2006
Journal article
Restricted
A story about formal methods adoption by a railway signaling Manufacturer
Bacherini S, Fantechi A, Tempestini M, Zingoni N
This paper reports the story of the introduction of formal methods in the development process of a railway signaling manufacturer. The first difficulty for a company is due to the many different formal methods proposals around; we show how this difficulty has been addressed and how the choice of a reference formal specification notation and of the related tools has been driven by many external factors related to the specific application domain, to the company policies, to european regulations. Cooperation with University has been fundamental in this process, which is now at the stage in which internal acceptance of the chosen formalisms and tools is established
Bacherini S, Fantechi A, Tempestini M, Zingoni N
This paper reports the story of the introduction of formal methods in the development process of a railway signaling manufacturer. The first difficulty for a company is due to the many different formal methods proposals around; we show how this difficulty has been addressed and how the choice of a reference formal specification notation and of the related tools has been driven by many external factors related to the specific application domain, to the company policies, to european regulations. Cooperation with University has been fundamental in this process, which is now at the stage in which internal acceptance of the chosen formalisms and tools is established
See at:
CNR IRIS | CNR IRIS | www.springerlink.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
2007
Journal article
Open Access
Behavioral complexity indicators for process algebra: the NKS approach
Bolognesi T
Several techniques for the experimental investigation of the computing power of various formal models, from cellular automata to Turing machines, have been proposed by S.Wolfram with his NKS (New Kind of Science). Visual complexity indicators reveal the 'internal shapes' of computations, and may expose constant, periodic, nested/fractal, pseudo-random, and even more sophisticated dynamics. In this paper we investigate visual complexity indicators for process algebra. With its emphasis on reactive, continuously observable behavior, as opposed to input/output behavior, process algebra might appear as an ideal candidate for NKS-style investigations; however, this formal model is in some sense more elaborate than the simple formalisms addressed in NKS, and poses specific problems, such as the presence of both events and states, and the explosive nature of non-determinism. We consider a set of process algebraic operators and prove its Turing universality by showing that they can emulate any elementary cellular automaton, including n. 110, which is itself universal. The correctness of the emulation is supported by an original visual indicator, which is then used for exploring various subclasses of algebraic expressions and their emergent features. Based on this indicator, and even by restricting to deterministic computations, we have detected and measured, by a data compression technique, the emergence of randomness in a subclass of expressions which is provably not universal. Besides providing a suggestive visualization of the relative strengths of operator subsets, we believe that results of this type, both of theoretical and of experimental nature, are desirable in light of one of the key NKS conjectures, according to which random-like behavior would be a witness of computational universality.Source: JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, vol. 72 (issue 1), pp. 50-77
DOI: 10.1016/j.jlap.2007.02.004
Metrics:
Bolognesi T
Several techniques for the experimental investigation of the computing power of various formal models, from cellular automata to Turing machines, have been proposed by S.Wolfram with his NKS (New Kind of Science). Visual complexity indicators reveal the 'internal shapes' of computations, and may expose constant, periodic, nested/fractal, pseudo-random, and even more sophisticated dynamics. In this paper we investigate visual complexity indicators for process algebra. With its emphasis on reactive, continuously observable behavior, as opposed to input/output behavior, process algebra might appear as an ideal candidate for NKS-style investigations; however, this formal model is in some sense more elaborate than the simple formalisms addressed in NKS, and poses specific problems, such as the presence of both events and states, and the explosive nature of non-determinism. We consider a set of process algebraic operators and prove its Turing universality by showing that they can emulate any elementary cellular automaton, including n. 110, which is itself universal. The correctness of the emulation is supported by an original visual indicator, which is then used for exploring various subclasses of algebraic expressions and their emergent features. Based on this indicator, and even by restricting to deterministic computations, we have detected and measured, by a data compression technique, the emergence of randomness in a subclass of expressions which is provably not universal. Besides providing a suggestive visualization of the relative strengths of operator subsets, we believe that results of this type, both of theoretical and of experimental nature, are desirable in light of one of the key NKS conjectures, according to which random-like behavior would be a witness of computational universality.Source: JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, vol. 72 (issue 1), pp. 50-77
DOI: 10.1016/j.jlap.2007.02.004
Metrics:
See at:
The Journal of Logic and Algebraic Programming | biblioproxy.cnr.it | CNR IRIS | CNR IRIS
2007
Journal article
Open Access
Infinite unfair shuffles and associativity
Ter Beek M. H., Kleijn J.
We consider a general shuffling operation for finite and infinite words which is not necessarily fair. This means that it may be the case that in a shuffle of two words, from some point onwards, one of these words prevails ad infinitum even though the other word still has letters to contribute. Prefixes and limits of shuffles are investigated, leading to a characterization of general shuffles in terms of shuffles of finite words, a result which does not hold for fair shuffles. Associativity of shuffling is an immediate corollary.Source: THEORETICAL COMPUTER SCIENCE, vol. 380 (issue 3), pp. 401-410
DOI: 10.1016/j.tcs.2007.03.030
Metrics:
Ter Beek M. H., Kleijn J.
We consider a general shuffling operation for finite and infinite words which is not necessarily fair. This means that it may be the case that in a shuffle of two words, from some point onwards, one of these words prevails ad infinitum even though the other word still has letters to contribute. Prefixes and limits of shuffles are investigated, leading to a characterization of general shuffles in terms of shuffles of finite words, a result which does not hold for fair shuffles. Associativity of shuffling is an immediate corollary.Source: THEORETICAL COMPUTER SCIENCE, vol. 380 (issue 3), pp. 401-410
DOI: 10.1016/j.tcs.2007.03.030
Metrics:
See at:
Theoretical Computer Science | CNR IRIS | CNR IRIS | www.sciencedirect.com
2007
Journal article
Metadata Only Access
Planar trivalent network computation
Bolognesi T.
Confluent rewrite systems for giant trivalent networks have been investigated by S. Wolfram as possible models of space and spacetime, in the ambitious search for the most fundamental, computational laws of physics. We restrict here to planar trivalent nets, which are shown to support Turing-complete computations, and take an even more radical, approach: while operating on network duals, we use just one elementary rewrite rule and drive its application by a simple, fully deterministic algorithm, rather than by pattern-matching. We devise effective visual indicators for exploring the complexity of computations with elementary initial conditions, consisting of thousands of graphs, and expose a rich variety of behaviors, from regular to random-like. Among their features we study, in particular, the dimensionality of the emergent space.
Bolognesi T.
Confluent rewrite systems for giant trivalent networks have been investigated by S. Wolfram as possible models of space and spacetime, in the ambitious search for the most fundamental, computational laws of physics. We restrict here to planar trivalent nets, which are shown to support Turing-complete computations, and take an even more radical, approach: while operating on network duals, we use just one elementary rewrite rule and drive its application by a simple, fully deterministic algorithm, rather than by pattern-matching. We devise effective visual indicators for exploring the complexity of computations with elementary initial conditions, consisting of thousands of graphs, and expose a rich variety of behaviors, from regular to random-like. Among their features we study, in particular, the dimensionality of the emergent space.
See at:
CNR IRIS
2007
Journal article
Restricted
On Competence in CD Grammar Systems with Parallel Rewriting
Ter Beek M H, Csuhajvarju E, Holzer M, Vaszil G
We continue our investigation of the generative power of cooperating distributed grammar systems (CDGSs), using the previously introduced <=k-, =k-, and >=k-competence-based cooperation strategies and context-free components that rewrite the sentential form in a parallel manner. This leads to new characterizations of the languages generated by (random context) ET0L systems and recurrent programmed grammars.Source: INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, vol. 18 (issue 6), pp. 1425-1439
DOI: 10.1142/s0129054107005467
Metrics:
Ter Beek M H, Csuhajvarju E, Holzer M, Vaszil G
We continue our investigation of the generative power of cooperating distributed grammar systems (CDGSs), using the previously introduced <=k-, =k-, and >=k-competence-based cooperation strategies and context-free components that rewrite the sentential form in a parallel manner. This leads to new characterizations of the languages generated by (random context) ET0L systems and recurrent programmed grammars.Source: INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, vol. 18 (issue 6), pp. 1425-1439
DOI: 10.1142/s0129054107005467
Metrics:
See at:
International Journal of Foundations of Computer Science | CNR IRIS | CNR IRIS | www.worldscinet.com
2003
Conference article
Restricted
Remarks on Turbo ASMs for Functional Equations and Recursion Schemes
Boerger E, Bolognesi T
The question raised in [15] is answered how to naturally model widely used forms of recursion by abstract machines. We show that turbo ASMs as defined in [7] allow one to faithfully reflect the common intuitive single-agent understanding of recursion. The argument is illustrated by turbo ASMs for Mergesort and Quicksort. Using turbo ASMs for returning function values allows one to seamlessly integrate functional description and programming techniques into the high-level 'abstract programming' by state transforming ASM rules.
Boerger E, Bolognesi T
The question raised in [15] is answered how to naturally model widely used forms of recursion by abstract machines. We show that turbo ASMs as defined in [7] allow one to faithfully reflect the common intuitive single-agent understanding of recursion. The argument is illustrated by turbo ASMs for Mergesort and Quicksort. Using turbo ASMs for returning function values allows one to seamlessly integrate functional description and programming techniques into the high-level 'abstract programming' by state transforming ASM rules.
2003
Conference article
Restricted
Team automata satisfying compositionality
Ter Beek M, Kleijn J
A team automaton is said to satisfy compositionality if its behaviour can be described in terms of the behaviour of its constituting component automata. As an initial investigation of the conditions under which team automata satisfy compositionality, we study their computations and behaviour in relation to those of their constituting component automata. We show that the construction of team automata according to certain natural types of synchronization guarantees compositionality.DOI: 10.1007/978-3-540-45236-2_22
Metrics:
Ter Beek M, Kleijn J
A team automaton is said to satisfy compositionality if its behaviour can be described in terms of the behaviour of its constituting component automata. As an initial investigation of the conditions under which team automata satisfy compositionality, we study their computations and behaviour in relation to those of their constituting component automata. We show that the construction of team automata according to certain natural types of synchronization guarantees compositionality.DOI: 10.1007/978-3-540-45236-2_22
Metrics:
See at:
doi.org | CNR IRIS | CNR IRIS | link.springer.com
2003
Conference article
Open Access
Teams of Pushdown Automata
Ter Beek M H, Csuhajvarju E, Mitrana V
We introduce team pushdown automata as a theoretical framework capable of modelling various communication and cooperation strategies in complex, distributed systems. Team pushdown automata are obtained by augmenting distributed pushdown automata with the notion of team cooperation or - alternatively - by augmenting team automata with pushdown memory. Here we study their accepting capacity.DOI: 10.1007/978-3-540-39866-0_32
DOI: 10.1080/00207160310001650099
Metrics:
Ter Beek M H, Csuhajvarju E, Mitrana V
We introduce team pushdown automata as a theoretical framework capable of modelling various communication and cooperation strategies in complex, distributed systems. Team pushdown automata are obtained by augmenting distributed pushdown automata with the notion of team cooperation or - alternatively - by augmenting team automata with pushdown memory. Here we study their accepting capacity.DOI: 10.1007/978-3-540-39866-0_32
DOI: 10.1080/00207160310001650099
Metrics:
See at:
International Journal of Computer Mathematics | doi.org | International Journal of Computer Mathematics | CNR IRIS | CNR IRIS | www.scopus.com
2003
Conference article
Restricted
AGILE: Software Architecture for Mobility
Andrade L, Baldan P, Baumeister H, Bruni R, Corradini A, De Nicola R, Fiadeiro Jl, Gadducci F, Gnesi S, Hoffman P, Koch N, Kosiuczenko P, Lapadula A, Latella D, Lopes A, Loreti M, Massink M, Mazzanti F, Montanari U, Oliveira C, Pugliese R, Tarlecki A, Wermerlinger M, Wirsing M, Zawoloxk A
Architecture-based approaches have been promoted as a means of controlling the complexity of system construction and evolution, in particular for providing systems with the agility required to operate in turbulent environments and to adapt very quickly to changes in the enterprise world. Recent technological advances in communication and distribution have made mobility an additional factor of complexity, one for which current architectural concepts and techniques can be hardly used. The AGILE project is developing an architectural approach in which mobility aspects can be modelled explicitly and mapped on the distribution and communication topology made available at physical levels. The whole approach is developed over a uniform mathematical framework based on graph-oriented techniques that support sound methodological principles, formal analysis, and re nement. This paper describes the AGILE project and some of the results gained during the rst project year.DOI: 10.1007/978-3-540-40020-2_1
Metrics:
Andrade L, Baldan P, Baumeister H, Bruni R, Corradini A, De Nicola R, Fiadeiro Jl, Gadducci F, Gnesi S, Hoffman P, Koch N, Kosiuczenko P, Lapadula A, Latella D, Lopes A, Loreti M, Massink M, Mazzanti F, Montanari U, Oliveira C, Pugliese R, Tarlecki A, Wermerlinger M, Wirsing M, Zawoloxk A
Architecture-based approaches have been promoted as a means of controlling the complexity of system construction and evolution, in particular for providing systems with the agility required to operate in turbulent environments and to adapt very quickly to changes in the enterprise world. Recent technological advances in communication and distribution have made mobility an additional factor of complexity, one for which current architectural concepts and techniques can be hardly used. The AGILE project is developing an architectural approach in which mobility aspects can be modelled explicitly and mapped on the distribution and communication topology made available at physical levels. The whole approach is developed over a uniform mathematical framework based on graph-oriented techniques that support sound methodological principles, formal analysis, and re nement. This paper describes the AGILE project and some of the results gained during the rst project year.DOI: 10.1007/978-3-540-40020-2_1
Metrics:
See at:
doi.org | CNR IRIS | CNR IRIS | link.springer.com | www.scopus.com
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.DOI: 10.1007/b13229
Metrics:
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.DOI: 10.1007/b13229
Metrics:
See at:
CNR IRIS | link.springer.com | doi.org | CNR IRIS