2001
Journal article
Unknown
Metric semantics for true concurrent real time
Katoen J. P., 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 254 (2001): 501–542.
Katoen J. P., 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 254 (2001): 501–542.
See at: CNR ExploRA
2004
Conference article
Unknown
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.Source: 8th DASIA 2004 DAta Systems In Aerospace, Nice, France, 28 June - 1 July 2004
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.Source: 8th DASIA 2004 DAta Systems In Aerospace, Nice, France, 28 June - 1 July 2004
See at: CNR ExploRA
2004
Report
Unknown
Model Checking Dependability Attributes of Wireless Group Communication. Full Version
Massink M., Katoen J., Latella D.
Models used for the analysis of dependability and performance attributes of communication protocols often abstract considerably from the details of the actual protocol. These models often consist of concurrent sub-models and this may make it hard to judge whether their behaviour is faithfully reflecting the protocol. In this paper, we show how model checking of continuous-time Markov chains, generated from high-level specifications, facilitates the analysis of both correctness and dependability attributes. We illustrate this by revisiting a performance analysis of a variant of the central access protocol of the IEEE 802.11 standard for wireless local area networks. This variant has been developed to support real-time group communication between autonomous mobile stations. Correctness and dependability properties are formally characterised using Continuous Stochastic Logic and are automatically verified by the ETMCC model checker. The models used are specified as Stochastic Activity Nets.Source: ISTI Technical reports, pp.1–18, 2004
Massink M., Katoen J., Latella D.
Models used for the analysis of dependability and performance attributes of communication protocols often abstract considerably from the details of the actual protocol. These models often consist of concurrent sub-models and this may make it hard to judge whether their behaviour is faithfully reflecting the protocol. In this paper, we show how model checking of continuous-time Markov chains, generated from high-level specifications, facilitates the analysis of both correctness and dependability attributes. We illustrate this by revisiting a performance analysis of a variant of the central access protocol of the IEEE 802.11 standard for wireless local area networks. This variant has been developed to support real-time group communication between autonomous mobile stations. Correctness and dependability properties are formally characterised using Continuous Stochastic Logic and are automatically verified by the ETMCC model checker. The models used are specified as Stochastic Activity Nets.Source: ISTI Technical reports, pp.1–18, 2004
See at: CNR ExploRA
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 30 (1998): 925–950. doi:10.1016/S0169-7552(97)00134-7
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 30 (1998): 925–950. doi:10.1016/S0169-7552(97)00134-7
DOI: 10.1016/s0169-7552(97)00134-7
Metrics:
See at:
Computer Networks and ISDN Systems 
| Computer Networks and ISDN Systems | NARCIS | NARCIS | www.sciencedirect.com | CNR ExploRA
1995
Journal article
Open Access
A stochastic causality-based process algebra
Brinksma E., Katoen J. P., 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 38 (1995): 552–565. doi:10.1093/comjnl/38.7.552
DOI: 10.1093/comjnl/38.7.552
Metrics:
Brinksma E., Katoen J. P., 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 38 (1995): 552–565. doi:10.1093/comjnl/38.7.552
DOI: 10.1093/comjnl/38.7.552
Metrics:
See at:
The Computer Journal 
| The Computer Journal | The Computer Journal | NARCIS | academic.oup.com | NARCIS | CNR ExploRA
1993
Journal article
Unknown
Definizione di linguaggi di specifica visuali: L'esperienza G-LOTOS
Latella D
Source: Rivista di Informatica XXIII (1993): 205–220.
Latella D
Source: Rivista di Informatica XXIII (1993): 205–220.
See at: CNR ExploRA
1991
Journal article
Unknown
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 22 (1991): 61–77.
Bolognesi T., Hagsang O., Latella D, Pehrson B.
An abstract is not availableSource: Computer networks and ISDN systems 22 (1991): 61–77.
See at: CNR ExploRA
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.Source: Rigorous Software Engineering for Service-Oriented Systems. Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing, edited by Martin Wirsing, Matthias Hölzl, pp. 522–540. Berlin: Springer, 2011
DOI: 10.1007/978-3-642-20401-2_25
Project(s): SENSORIA
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.Source: Rigorous Software Engineering for Service-Oriented Systems. Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing, edited by Martin Wirsing, Matthias Hölzl, pp. 522–540. Berlin: Springer, 2011
DOI: 10.1007/978-3-642-20401-2_25
Project(s): SENSORIA
Metrics:
See at:
NARCIS | NARCIS | doi.org | link.springer.com | CNR ExploRA
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
Unknown
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.Source: ICALP 1998, pp. 568–579, 01/07/1998
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.Source: ICALP 1998, pp. 568–579, 01/07/1998
See at: CNR ExploRA
1997
Conference article
Unknown
Stochastic analysis via a probabilistic process algebra
Latella D, P. Quaglia
Source: PAPM 1997, pp. 187–206, 1997
Latella D, P. Quaglia
Source: PAPM 1997, pp. 187–206, 1997
See at: CNR ExploRA
1996
Conference article
Unknown
On specifying real-time systems in a causality-based setting
Katoen J. P., Latella D, Langerak R, Brinksma E
Source: 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 385–404, Uppsala, 1996
Katoen J. P., Latella D, Langerak R, Brinksma E
Source: 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 385–404, Uppsala, 1996
See at: CNR ExploRA
1996
Conference article
Unknown
Stochastic simulation of event structures
Katoen J. P, Brinksma E, Latella D, Langerak R
Source: 4th workshop on process algebras and performance modeling, pp. 21–40, Torino, 1996
Katoen J. P, Brinksma E, Latella D, Langerak R
Source: 4th workshop on process algebras and performance modeling, pp. 21–40, Torino, 1996
See at: CNR ExploRA
1994
Conference article
Unknown
Modeling systems by probabilistic process algebra: an event structures approach
Katoen J. P., Langerak R., Latella D.
An abstract is not available.Source: FORTE '93, pp. 253–268, 1994
Katoen J. P., Langerak R., Latella D.
An abstract is not available.Source: FORTE '93, pp. 253–268, 1994
See at: CNR ExploRA
1994
Contribution to book
Unknown
Performance analysis and true concurrency semantics
Brinksma E., Katoen J. P., Langerak R., Latella D.
An abstract is not available.Source: Theories and Experiences for Real-Time System Development, pp. 309–337. Singapore: World Scientific, 1994
Brinksma E., Katoen J. P., Langerak R., Latella D.
An abstract is not available.Source: Theories and Experiences for Real-Time System Development, pp. 309–337. Singapore: World Scientific, 1994
See at: CNR ExploRA
1994
Conference article
Unknown
Performance analysis and true concurrency semantics (extended abstract)
Brinksma E., Katoen J. P., Langerak R., Latella D.
An abstract is not available.Source: 2nd workshop on process algebras and performance modeling, pp. 157–174, Erlangen, 1994
Brinksma E., Katoen J. P., Langerak R., Latella D.
An abstract is not available.Source: 2nd workshop on process algebras and performance modeling, pp. 157–174, Erlangen, 1994
See at: CNR ExploRA
1993
Conference article
Unknown
Gate splitting in LOTOS specifications using abstract interpretation
Giannotti F, Latella D
Source: TAPSOFT '93, pp. 437–452, Orsay, 1993
Giannotti F, Latella D
Source: TAPSOFT '93, pp. 437–452, Orsay, 1993
See at: CNR ExploRA
1992
Conference article
Unknown
Using abstract interpretation for gate splitting in LOTOS specifications (extended abstract)
Giannotti F, Latella D
Source: Journees de travail WSA'92 Analyse Statique, pp. 194–204, 1992
Giannotti F, Latella D
Source: Journees de travail WSA'92 Analyse Statique, pp. 194–204, 1992
See at: CNR ExploRA
1991
Conference article
Unknown
Non-standard interpretations of LOTOS specifications
Bolognesi T, Latella D, Zuppa E
Source: TAPSOFT '91, pp. 217–231, Brighton, 1991
Bolognesi T, Latella D, Zuppa E
Source: TAPSOFT '91, pp. 217–231, Brighton, 1991
See at: CNR ExploRA
1989
Conference article
Unknown
Shared abstract data types: An algebraic methodology for their specification
Bondavalli A, De Francesco N, Latella D, Vaglini G
Source: 2nd Symposium on Mathematical Foundation of Database Theory, pp. 53–67, Visegrad, 1989
Bondavalli A, De Francesco N, Latella D, Vaglini G
Source: 2nd Symposium on Mathematical Foundation of Database Theory, pp. 53–67, Visegrad, 1989
See at: CNR ExploRA