2001
Journal article
Restricted
Dependability analysis in the early phases of UML based system design.
Bondavalli A, Dal Cin M, Latella D, Majzik I, Pataricza A, Savoia G
An abstract is not available.Source: COMPUTER SYSTEMS SCIENCE AND ENGINEERING, vol. 16 (issue 5), pp. 265-275
Bondavalli A, Dal Cin M, Latella D, Majzik I, Pataricza A, Savoia G
An abstract is not available.Source: COMPUTER SYSTEMS SCIENCE AND ENGINEERING, vol. 16 (issue 5), pp. 265-275
2001
Journal article
Restricted
Metric semantics for true concurrent real time
Katoen Jp, Baier C, Latella D
This paper investigates the use of a complete metric space framework for providing denotational semantics to a real-time process algebra. The study is carried out in a non-interleaving setting and is based on a timed extension of Langerak's bundle event structures, a variant of Winskel's event structures. The distance function of the metric is based on the amount of time to which event structures do 'agree'. We show that this intuitive notion of distance is a pseudo-metric (but not a metric) on the set of timed event structures. A generalisation to equivalence classes of timed event structures in which we abstract from event identities and non-executable events (events that can never occur) is shown to be a complete ultra-metric space. We present an operational semantics for the considered language and show that the metric semantics is an abstraction of it. The operational semantics is characterised by the absence of synchronisation on the advance of time as opposed to the operational semantics of most real-time calculi. The consistency between our metric and an existing cpo-based denotational semantics is briefly investigated.Source: THEORETICAL COMPUTER SCIENCE, vol. 254 (issue 1-2), pp. 501-542
Katoen Jp, Baier C, Latella D
This paper investigates the use of a complete metric space framework for providing denotational semantics to a real-time process algebra. The study is carried out in a non-interleaving setting and is based on a timed extension of Langerak's bundle event structures, a variant of Winskel's event structures. The distance function of the metric is based on the amount of time to which event structures do 'agree'. We show that this intuitive notion of distance is a pseudo-metric (but not a metric) on the set of timed event structures. A generalisation to equivalence classes of timed event structures in which we abstract from event identities and non-executable events (events that can never occur) is shown to be a complete ultra-metric space. We present an operational semantics for the considered language and show that the metric semantics is an abstraction of it. The operational semantics is characterised by the absence of synchronisation on the advance of time as opposed to the operational semantics of most real-time calculi. The consistency between our metric and an existing cpo-based denotational semantics is briefly investigated.Source: THEORETICAL COMPUTER SCIENCE, vol. 254 (issue 1-2), pp. 501-542
2004
Conference article
Restricted
PRIDE: an integrated software development environment for dependable systems
Mazzini S, Latella D, Viva D
This paper presents the PRIDE research project, developed by Intecs and co-funded by the Italian Space Agency. The project aims at providing an integrated software development environment for dependable systems based on UML, which integrates design activities with selected methods for formal verification and validation (V&V) and quantitative dependability attributes assessment, supported by appropriate tools. The PRIDE environment is built as an extension of the already existing environment for the modeling of Hard Real Time systems, HRT-UML, based on the Unified Modeling Language (UML) notation. The outcome is an advanced and integrated methodological solution for the design of complex embedded real-time systems and for their evaluation and verification, according to rigorous techniques based on formal theories, such as formal verification, model based dependability evaluation and schedulability analysis.
Mazzini S, Latella D, Viva D
This paper presents the PRIDE research project, developed by Intecs and co-funded by the Italian Space Agency. The project aims at providing an integrated software development environment for dependable systems based on UML, which integrates design activities with selected methods for formal verification and validation (V&V) and quantitative dependability attributes assessment, supported by appropriate tools. The PRIDE environment is built as an extension of the already existing environment for the modeling of Hard Real Time systems, HRT-UML, based on the Unified Modeling Language (UML) notation. The outcome is an advanced and integrated methodological solution for the design of complex embedded real-time systems and for their evaluation and verification, according to rigorous techniques based on formal theories, such as formal verification, model based dependability evaluation and schedulability analysis.
1998
Journal article
Restricted
Partial order models for quantitative extensions of LOTOS
Brinksma E, Katoen J, Langerak R, Latella D
Event structures are a prominent model for non-interleaving concurrency. The use of event structures for providing a compositional non-interleaving semantics to LOTOS without data is studied. In particular, several quantitative extensions of event structures are proposed that incorporate notions like time - both of deterministic and stochastic nature - and probability. The suitability of these models for giving a non-interleaving semantics to a timed, stochastic and probabilistic extension of LOTOS is investigated. Consistency between the event structure semantics and an ?event-based. operational semantics is addressed for the different quantitative variants of LOTOS and is worked out for the timed case in more detail. These consistency results facilitate the coherent use of an interleaving and a non-interleaving semantic view in a single design trajectory and provide a justification for the event structure semantics. As a running example an infinite buffer is used in which gradually timing constraints on latency and rates of accepting and producing data and the probability of loss of messages are incorporated.Source: COMPUTER NETWORKS AND ISDN SYSTEMS, vol. 30 (issue 9-10), pp. 925-950
DOI: 10.1016/s0169-7552(97)00134-7
Metrics:
Brinksma E, Katoen J, Langerak R, Latella D
Event structures are a prominent model for non-interleaving concurrency. The use of event structures for providing a compositional non-interleaving semantics to LOTOS without data is studied. In particular, several quantitative extensions of event structures are proposed that incorporate notions like time - both of deterministic and stochastic nature - and probability. The suitability of these models for giving a non-interleaving semantics to a timed, stochastic and probabilistic extension of LOTOS is investigated. Consistency between the event structure semantics and an ?event-based. operational semantics is addressed for the different quantitative variants of LOTOS and is worked out for the timed case in more detail. These consistency results facilitate the coherent use of an interleaving and a non-interleaving semantic view in a single design trajectory and provide a justification for the event structure semantics. As a running example an infinite buffer is used in which gradually timing constraints on latency and rates of accepting and producing data and the probability of loss of messages are incorporated.Source: COMPUTER NETWORKS AND ISDN SYSTEMS, vol. 30 (issue 9-10), pp. 925-950
DOI: 10.1016/s0169-7552(97)00134-7
Metrics:
See at:
Computer Networks and ISDN Systems 
| CNR IRIS | CNR IRIS | Computer Networks and ISDN Systems | NARCIS | NARCIS | www.sciencedirect.com
1995
Journal article
Open Access
A stochastic causality-based process algebra
Brinksma E, Katoen Jp, Langerak R, Latella D
This paper discusses stochastic extensions of a simple process algebra in a causality-based setting. Atomic actions are supposed to happen after a delay that is determined by a stochastic variable with a certain distribution. A simple stochastic type of event structures is discussed, restricting the distribution functions to be exponential. A corresponding operational semantics of this model is given and compared to existing (interleaved) approaches. Secondly, a stochastic variant of event structures is discussed where distributions are of a much more general nature, viz. of phase-type. This includes exponential, Erlang, Coxian and mixtures of exponential distributions.Source: THE COMPUTER JOURNAL, vol. 38 (issue 7), pp. 552-565
DOI: 10.1093/comjnl/38.7.552
Metrics:
Brinksma E, Katoen Jp, Langerak R, Latella D
This paper discusses stochastic extensions of a simple process algebra in a causality-based setting. Atomic actions are supposed to happen after a delay that is determined by a stochastic variable with a certain distribution. A simple stochastic type of event structures is discussed, restricting the distribution functions to be exponential. A corresponding operational semantics of this model is given and compared to existing (interleaved) approaches. Secondly, a stochastic variant of event structures is discussed where distributions are of a much more general nature, viz. of phase-type. This includes exponential, Erlang, Coxian and mixtures of exponential distributions.Source: THE COMPUTER JOURNAL, vol. 38 (issue 7), pp. 552-565
DOI: 10.1093/comjnl/38.7.552
Metrics:
See at:
The Computer Journal 
| The Computer Journal | The Computer Journal | NARCIS | academic.oup.com | CNR IRIS | CNR IRIS | NARCIS
1993
Journal article
Metadata Only Access
Definizione di linguaggi di specifica visuali: L'esperienza G-LOTOS
Latella D
Source: RIVISTA DI INFORMATICA, vol. XXIII (issue 3), pp. 205-220
Latella D
Source: RIVISTA DI INFORMATICA, vol. XXIII (issue 3), pp. 205-220
See at:
CNR IRIS
1991
Journal article
Metadata Only Access
The definition of a graphical G-LOTOS editor using the meta-tool LOGGIE
Bolognesi T, Hagsang O, Latella D, Pehrson B
An abstract is not availableSource: COMPUTER NETWORKS AND ISDN SYSTEMS, vol. 22, pp. 61-77
Bolognesi T, Hagsang O, Latella D, Pehrson B
An abstract is not availableSource: COMPUTER NETWORKS AND ISDN SYSTEMS, vol. 22, pp. 61-77
See at:
CNR IRIS
1988
Journal article
Closed Access
The osiride directory system: status and perspectives
Latella D, Lenzini L
This paper outlines some design aspects of the Distributed Directory System which will run in the framework of the OSIRIDE project. The aspects related to distributed name resolution will be enphasized and the main ideas for an efficient algorithm, which makes use of a particular kind of cache in the distributed representation of the name space, will be sketched. The first version of the OSIRIDE Directory System will be implemented and tested on a system made up of a cluster of IBM PCs (XT and AT) connected to the IBM Token Ring Local Area Network.Source: COMPUTER STANDARDS & INTERFACES, vol. 7 (issue 1-2), pp. 111-118
DOI: 10.1016/0920-5489(88)90055-4
Metrics:
Latella D, Lenzini L
This paper outlines some design aspects of the Distributed Directory System which will run in the framework of the OSIRIDE project. The aspects related to distributed name resolution will be enphasized and the main ideas for an efficient algorithm, which makes use of a particular kind of cache in the distributed representation of the name space, will be sketched. The first version of the OSIRIDE Directory System will be implemented and tested on a system made up of a cluster of IBM PCs (XT and AT) connected to the IBM Token Ring Local Area Network.Source: COMPUTER STANDARDS & INTERFACES, vol. 7 (issue 1-2), pp. 111-118
DOI: 10.1016/0920-5489(88)90055-4
Metrics:
See at:
Computer Standards & Interfaces | CNR IRIS | www.sciencedirect.com
2011
Contribution to book
Open Access
Quantitative Analysis of Services
Cappello I, Clark A, Gilmore S, Latella D, Loreti M, Quaglia P, Schivo S
We show a number of applications of the tools which have been developed within the sensoria project to perform quantitative analysis of services. These tools are formally grounded on source calculi which allow the description of services at distinct levels of abstraction, and hence pose distinct challenges to both modelling and analysis. The reported applications refer to (suitable subcomponents of) the Finance Case-Study, and show instances of, respectively, exact model checking of MarCaSPiS against the both state-aware and action-aware logic SoSL, exact and statistical model checking of sCOWS against the state-aware logic CSL, querying of PEPA models by terms of the XSP language that expresses both state-aware and action-aware stochastic probes.DOI: 10.1007/978-3-642-20401-2_25
Project(s): Software Engineering for Service-Oriented Overlay Computers
Metrics:
Cappello I, Clark A, Gilmore S, Latella D, Loreti M, Quaglia P, Schivo S
We show a number of applications of the tools which have been developed within the sensoria project to perform quantitative analysis of services. These tools are formally grounded on source calculi which allow the description of services at distinct levels of abstraction, and hence pose distinct challenges to both modelling and analysis. The reported applications refer to (suitable subcomponents of) the Finance Case-Study, and show instances of, respectively, exact model checking of MarCaSPiS against the both state-aware and action-aware logic SoSL, exact and statistical model checking of sCOWS against the state-aware logic CSL, querying of PEPA models by terms of the XSP language that expresses both state-aware and action-aware stochastic probes.DOI: 10.1007/978-3-642-20401-2_25
Project(s): Software Engineering for Service-Oriented Overlay Computers
Metrics:
See at:
NARCIS | NARCIS | doi.org | CNR IRIS | CNR IRIS | link.springer.com
1994
Contribution to book
Unknown
Performance analysis and true concurrency semantics
E. Brinksma, J. P. Katoen, R. Langerak, Latella D
Source: Theories and Experiences for Real-Time System Development, edited by T. RUS AND C. RATRAY, pp. 309–337. Londra: World Scientific Publishing, 1994
E. Brinksma, J. P. Katoen, R. Langerak, Latella D
Source: Theories and Experiences for Real-Time System Development, edited by T. RUS AND C. RATRAY, pp. 309–337. Londra: World Scientific Publishing, 1994
See at: CNR ExploRA
1998
Conference article
Restricted
Metric semantics for true concurrent real time (Ext. Abs.)
Baier C, Katoen J, Latella D
This paper investigates the use of a complete metric space framework for providing denotational semantics to a real-time process algebra. The study is carried out in a non-interleaving setting and is based on a timed extension of Langerak's bundle event structures, a variant of Winskel's event structures. The distance function of the metric is based on the amount of time to which event structures do 'agree'. We show that this intuitive notion of distance is a pseudo-metric (but not a metric) on the set of timed event structures. A generalisation to equivalence classes of timed event structures in which we abstract from event identities and non-executable events (events that can never occur) is shown to be a complete ultra-metric space. We present an operational semantics for the considered language and show that the metric semantics is an abstraction of it. The operational semantics is characterised by the absence of synchronisation on the advance of time as opposed to the operational semantics of most real-time calculi. The consistency between our metric and an existing cpo-based denotational semantics is briefly investigated.
Baier C, Katoen J, Latella D
This paper investigates the use of a complete metric space framework for providing denotational semantics to a real-time process algebra. The study is carried out in a non-interleaving setting and is based on a timed extension of Langerak's bundle event structures, a variant of Winskel's event structures. The distance function of the metric is based on the amount of time to which event structures do 'agree'. We show that this intuitive notion of distance is a pseudo-metric (but not a metric) on the set of timed event structures. A generalisation to equivalence classes of timed event structures in which we abstract from event identities and non-executable events (events that can never occur) is shown to be a complete ultra-metric space. We present an operational semantics for the considered language and show that the metric semantics is an abstraction of it. The operational semantics is characterised by the absence of synchronisation on the advance of time as opposed to the operational semantics of most real-time calculi. The consistency between our metric and an existing cpo-based denotational semantics is briefly investigated.
1997
Conference article
Metadata Only Access
See at:
CNR IRIS
1996
Conference article
Metadata Only Access
On specifying real-time systems in a causality-based setting
Katoen Jp, Latella D, Langerak R, Brinksma E
Katoen Jp, Latella D, Langerak R, Brinksma E
See at:
CNR IRIS
1996
Conference article
Metadata Only Access
See at:
CNR IRIS
1994
Conference article
Metadata Only Access
Modeling systems by probabilistic process algebra: an event structures approach
Katoen Jp, Langerak R, Latella D
An abstract is not available.Source: IFIP TRANSACTIONS. C, COMMUNICATION SYSTEMS, pp. 253-268
Katoen Jp, Langerak R, Latella D
An abstract is not available.Source: IFIP TRANSACTIONS. C, COMMUNICATION SYSTEMS, pp. 253-268
See at:
CNR IRIS
1994
Contribution to book
Metadata Only Access
Performance analysis and true concurrency semantics
Brinksma E, Katoen Jp, Langerak R, Latella D
An abstract is not available.
Brinksma E, Katoen Jp, Langerak R, Latella D
An abstract is not available.
See at:
CNR IRIS
1994
Conference article
Metadata Only Access
Performance analysis and true concurrency semantics (extended abstract)
Brinksma E, Katoen Jp, Langerak R, Latella D
An abstract is not available.
Brinksma E, Katoen Jp, Langerak R, Latella D
An abstract is not available.
See at:
CNR IRIS
1993
Conference article
Metadata Only Access
See at:
CNR IRIS
1992
Conference article
Metadata Only Access
Using abstract interpretation for gate splitting in LOTOS specifications (extended abstract)
Giannotti F, Latella D
Giannotti F, Latella D
See at:
CNR IRIS
1991
Conference article
Metadata Only Access
See at:
CNR IRIS