2006
Journal article
Unknown
FMICS 2005 - 10th International Workshop on Formal Methods in SAfety Critical Systems
Massink M., Margaria T.
Report on the 10th edition of the FMICS international workshop held in Lisbon in 2005.Source: ERCIM news 64 (2006): 6–7.
Massink M., Margaria T.
Report on the 10th edition of the FMICS international workshop held in Lisbon in 2005.Source: ERCIM news 64 (2006): 6–7.
See at: CNR ExploRA
2010
Journal article
Open Access
Modelling interactive experience, function and performance in ubiquitous systems
Harrison M., Massink M.
The cost of deploying a ubiquitous system to enhance a physical environment is likely to be considerable. The success of its deployment is highly dependent on its context: the physical environment and the activities that are to be carried out within it. This paper provides an initial exploration of whether stochastic process algebras (in particular PEPA with a Fluid Flow semantics) might be used to explore consequences before deployment. The focus of the exploration is to aid understanding of how a proposed system supports users within the environment. The challenge is to provide notations and techniques that will enable the analysis of potentially complex systems.Source: Electronic notes in theoretical computer science 261 (2010): 23–42. doi:10.1016/j.entcs.2010.01.004
DOI: 10.1016/j.entcs.2010.01.004
Metrics:
Harrison M., Massink M.
The cost of deploying a ubiquitous system to enhance a physical environment is likely to be considerable. The success of its deployment is highly dependent on its context: the physical environment and the activities that are to be carried out within it. This paper provides an initial exploration of whether stochastic process algebras (in particular PEPA with a Fluid Flow semantics) might be used to explore consequences before deployment. The focus of the exploration is to aid understanding of how a proposed system supports users within the environment. The challenge is to provide notations and techniques that will enable the analysis of potentially complex systems.Source: Electronic notes in theoretical computer science 261 (2010): 23–42. doi:10.1016/j.entcs.2010.01.004
DOI: 10.1016/j.entcs.2010.01.004
Metrics:
See at:
Electronic Notes in Theoretical Computer Science 
| www.sciencedirect.com 
| CNR ExploRA
2007
Conference article
Restricted
Basic observables for probabilistic may testing
Palmeri M. C., De Nicola R., Massink M.
The definition of behavioural preorders over process terms as the maximal (pre-)congruences induced by basic observables has proven to be a useful technique to define various preorders and equivalences in the non-probabilistic setting. In this paper, we consider probabilistic observables to define an observational semantics for a probabilistic pro- cess calculus. The resulting pre-congruence is proven to coincide with a probabilistic may preorder, which, in turn, corresponds to a natural probabilistic extension of the may testing preorder of De Nicola and Hennessy.Source: Fourth International Conference on the Quantitative Evaluation of Systems, pp. 189–198, Edinburgh, Scotland, U.K., 17-19 September 2007
DOI: 10.1109/qest.2007.19
Metrics:
Palmeri M. C., De Nicola R., Massink M.
The definition of behavioural preorders over process terms as the maximal (pre-)congruences induced by basic observables has proven to be a useful technique to define various preorders and equivalences in the non-probabilistic setting. In this paper, we consider probabilistic observables to define an observational semantics for a probabilistic pro- cess calculus. The resulting pre-congruence is proven to coincide with a probabilistic may preorder, which, in turn, corresponds to a natural probabilistic extension of the may testing preorder of De Nicola and Hennessy.Source: Fourth International Conference on the Quantitative Evaluation of Systems, pp. 189–198, Edinburgh, Scotland, U.K., 17-19 September 2007
DOI: 10.1109/qest.2007.19
Metrics:
See at:
xplorestaging.ieee.org | CNR ExploRA
2002
Contribution to conference
Unknown
Continuous interaction with computers: issues and requirements
Massink M.
An abstract is not availableSource: FM&&T Day, Pisa, Italy, 2002
Massink M.
An abstract is not availableSource: FM&&T Day, Pisa, Italy, 2002
See at: CNR ExploRA
2003
Report
Open Access
D1.1 - Trends in Verification and Validation: Model Checking.
Massink. M.
In this chapter we highlight some of the more exciting recent advances and challenges in the development of model-checking technology.Source: Project report, AMSD, Deliverable D1.1, 2003
Massink. M.
In this chapter we highlight some of the more exciting recent advances and challenges in the development of model-checking technology.Source: Project report, AMSD, Deliverable D1.1, 2003
See at:
ISTI Repository | CNR ExploRA
2003
Other
Open Access
FM '03 Tutorial Notes
Massink M.
Tutorial Notes of the 12th International FME Symposium held in Pisa, September 8-12, 2003.
Massink M.
Tutorial Notes of the 12th International FME Symposium held in Pisa, September 8-12, 2003.
See at:
ISTI Repository | CNR ExploRA
2002
Report
Open Access
Introduction to UPPAAL slides
Massink M.
An abstract is not availableSource: ISTI Technical reports, 2002
Massink M.
An abstract is not availableSource: ISTI Technical reports, 2002
See at:
ISTI Repository | CNR ExploRA
2005
Contribution to conference
Unknown
Foreword - FMICS'05 Tenth International Workshop on Formal Methods for Industrial Critical Systems.
Margaria T., Massink M.
Foreword of the proceedings of the tenth edition of the International Workshop on Formal Methods for Industrial Critical Systems, Lisbon, 2005Source: New York: ACM, Association for computing machinery, 2005
Margaria T., Massink M.
Foreword of the proceedings of the tenth edition of the International Workshop on Formal Methods for Industrial Critical Systems, Lisbon, 2005Source: New York: ACM, Association for computing machinery, 2005
See at: CNR ExploRA
2007
Report
Unknown
TOCAI.IT - D7.1 - Process-oriented models and languages
Brogi A., Bruni R., Ciancarini P., Corradi A., Ferrari G., Massink M., Montanari U.
Project Report on the scientific results obtained in the first year (2007) by Activity 7 of FIRB project TOCAI.Source: Project report, TOCA.IT, Deliverable D7.1, 2007
Brogi A., Bruni R., Ciancarini P., Corradi A., Ferrari G., Massink M., Montanari U.
Project Report on the scientific results obtained in the first year (2007) by Activity 7 of FIRB project TOCAI.Source: Project report, TOCA.IT, Deliverable D7.1, 2007
See at: CNR ExploRA
2008
Report
Unknown
TOCAI - D7.2 - Process-oriented models and languages: scientific results and application scenarios
Brogi A., Bruni R., Ciancarini P., Corradi A., Ferrari G., Massink M., Montanari U.
Deliverable D7.2 of Activity 7 of the FIRB project TOCAI.ITSource: Project report, TOCAI, Deliverable D7.2, 2008
Brogi A., Bruni R., Ciancarini P., Corradi A., Ferrari G., Massink M., Montanari U.
Deliverable D7.2 of Activity 7 of the FIRB project TOCAI.ITSource: Project report, TOCAI, Deliverable D7.2, 2008
See at: CNR ExploRA
1999
Journal article
Restricted
The hybrid world of virtual environments
Smith S., Duke D., Massink M.
Much of the work concerned with virtual environments has addressed the development of new rendering technologies or interaction techniques. As the technology matures and becomes adopted in a wider range of applications, there is, however, a need to better understand how this technology can be accommodated in software engineering practice. A particular challenge presented by virtual environments is the complexity of the interaction that is supported, and sometimes necessary, for a particular task. Methods such as finite-state automata which are used to represent and design dialogue components for more conventional interfaces, e.g. using direct manipulation within a desktop model, do not seem to capture adequately the style of interaction that is afforded by richer input devices and graphical models. In this paper, we suggest that virtual environments are, fundamentally, what are known as hybrid systems. Building on this insight, we demonstrate how techniques developed for modelling hybrid systems can be used to represent and understand virtual interaction in a way that can be used in the specification and design phases of software development, and which have the potential to support prototyping and analysis of virtual interfaces.Source: Computer graphics forum (Print) 18 (1999): 297–307. doi:10.1111/1467-8659.00350
DOI: 10.1111/1467-8659.00350
Metrics:
Smith S., Duke D., Massink M.
Much of the work concerned with virtual environments has addressed the development of new rendering technologies or interaction techniques. As the technology matures and becomes adopted in a wider range of applications, there is, however, a need to better understand how this technology can be accommodated in software engineering practice. A particular challenge presented by virtual environments is the complexity of the interaction that is supported, and sometimes necessary, for a particular task. Methods such as finite-state automata which are used to represent and design dialogue components for more conventional interfaces, e.g. using direct manipulation within a desktop model, do not seem to capture adequately the style of interaction that is afforded by richer input devices and graphical models. In this paper, we suggest that virtual environments are, fundamentally, what are known as hybrid systems. Building on this insight, we demonstrate how techniques developed for modelling hybrid systems can be used to represent and understand virtual interaction in a way that can be used in the specification and design phases of software development, and which have the potential to support prototyping and analysis of virtual interfaces.Source: Computer graphics forum (Print) 18 (1999): 297–307. doi:10.1111/1467-8659.00350
DOI: 10.1111/1467-8659.00350
Metrics:
See at:
Computer Graphics Forum | onlinelibrary.wiley.com | www.scopus.com | CNR ExploRA
2009
Contribution to journal
Restricted
Preface. International Journal on Software Tools for Technology Transfer
Margaria T., Massink M.
Source: International journal on software tools for technology transfer (Print) 11 (2009): 355–357. doi:10.1007/s10009-009-0121-6
DOI: 10.1007/s10009-009-0121-6
Metrics:
Margaria T., Massink M.
Source: International journal on software tools for technology transfer (Print) 11 (2009): 355–357. doi:10.1007/s10009-009-0121-6
DOI: 10.1007/s10009-009-0121-6
Metrics:
See at:
link.springer.com | CNR ExploRA
2009
Contribution to journal
Unknown
Proceedings of the third international workshop on formal methods for interactive systems (FMIS 2009)
Harrison M., Massink M.
Special issue on the third international workshop on formal methods for interactive systems (FMIS 2009)
Harrison M., Massink M.
Special issue on the third international workshop on formal methods for interactive systems (FMIS 2009)
See at: CNR ExploRA
2005
Contribution to conference
Unknown
Proceedings of the Tenth International Workshop on Formal Methods for Industrial Critical Systems.
T. Margaria, M. Massink
Proceedings of the Tenth International Workshop on Formal Methods for Industrial Critical SystemsSource: New York: ACM, Association for computing machinery, 2005
T. Margaria, M. Massink
Proceedings of the Tenth International Workshop on Formal Methods for Industrial Critical SystemsSource: New York: ACM, Association for computing machinery, 2005
See at: CNR ExploRA
2001
Contribution to conference
Unknown
International Workshop on Continuity in Future Computer Systems, Apr. 23-24, 2001, Porto, Portugal
Doherty G., Massink M., Wilson M.
International Workshop on Continuity in Future Computer Systems
Doherty G., Massink M., Wilson M.
International Workshop on Continuity in Future Computer Systems
See at: CNR ExploRA
1999
Contribution to conference
Closed Access
Theoretical and practical aspects of SPIN model checking. 5th and 6th Int. SPIN workshops
Dams D., Gerth R., Leue S., Massink M.
Theoretical and practical aspects of SPIN model checkingSource: Berlin: Springer, 1999
DOI: 10.1007/3-540-48234-2
Metrics:
Dams D., Gerth R., Leue S., Massink M.
Theoretical and practical aspects of SPIN model checkingSource: Berlin: Springer, 1999
DOI: 10.1007/3-540-48234-2
Metrics:
See at:
doi.org | link.springer.com | CNR ExploRA
2000
Conference article
Unknown
Continuous interaction and human control
Doherty G., Massink M.
Modern information technology is becoming both increasingly ubiquitous and increasingly varied in the possible ways it can interact with the user. With many emerging technologies, interaction with the user is no longer based exclusively on discrete interactions, which are the underlying model for many traditional approaches in HCI (for example, Norman's seven stage model (Norman, 1998). Rather, modem interaction techniques develop towards interfaces where the user is in constant interaction with the computing system, communicating with it by means of gestures, speech and animation as well as discrete communication such as selection by pressing buttons or typing via a keyboard. This development requires new interface design approaches that allow for the analysis of the discrete as well as the continuous aspects of the interface, and that support reasoning about real-time issues. We examine how classical manual control theory can be applied in this area. Conversely, in the area of human control, a shift has occurred away from pure manual control scenarios to more supervisory and mixed control tasks. We believe these two trends have established much common ground between the areas of interactive· systems and human control, and examine some on-going research in this area.Source: XVIII European Annual Conference on Human Decision Making and Manual Control, pp. 80–96, Loughborough, October 25-27 1999
Doherty G., Massink M.
Modern information technology is becoming both increasingly ubiquitous and increasingly varied in the possible ways it can interact with the user. With many emerging technologies, interaction with the user is no longer based exclusively on discrete interactions, which are the underlying model for many traditional approaches in HCI (for example, Norman's seven stage model (Norman, 1998). Rather, modem interaction techniques develop towards interfaces where the user is in constant interaction with the computing system, communicating with it by means of gestures, speech and animation as well as discrete communication such as selection by pressing buttons or typing via a keyboard. This development requires new interface design approaches that allow for the analysis of the discrete as well as the continuous aspects of the interface, and that support reasoning about real-time issues. We examine how classical manual control theory can be applied in this area. Conversely, in the area of human control, a shift has occurred away from pure manual control scenarios to more supervisory and mixed control tasks. We believe these two trends have established much common ground between the areas of interactive· systems and human control, and examine some on-going research in this area.Source: XVIII European Annual Conference on Human Decision Making and Manual Control, pp. 80–96, Loughborough, October 25-27 1999
See at: CNR ExploRA
1997
Conference article
Unknown
Investigating the behaviour of PREMO synchronisable objects
Faconti G, Massink M
Source: Design, Specification and Verification of Interactive Systems '97, pp. 125–141, Granada, E, June 4-6, 1997
Faconti G, Massink M
Source: Design, Specification and Verification of Interactive Systems '97, pp. 125–141, Granada, E, June 4-6, 1997
See at: CNR ExploRA
1993
Conference article
Restricted
Completeness of the equational semantics for basic LOTOS
Massink M, Rooijakkers L.
The logical correspondence between the equational semantics of Basic LOTOS and is standard, derivational one is proven. A derivational semantics is traditionally given by means of a set of axioms and deduction rules which define a deduction system. With such semantics, some difficulties arise when dealing with deduction rules with negative premises; also, the proof that a transition cannot take place cannot be carried out within the formal system. On the other hand, in the equational semantics approach, a transition is viewed as the application of a triadic predicate. Such a function is defined by a set of equations, and this, in a natural way, allows for the use of negative information within the system. It is shown that for Basic LOTOS, when restricted to guarded recursion, both formal reasoning systems strongly correspondSource: Fourth Workshop on Future Trends of Distributed Computing Systems, pp. 396–403, 1993
DOI: 10.1109/ftdcs.1993.344208
Metrics:
Massink M, Rooijakkers L.
The logical correspondence between the equational semantics of Basic LOTOS and is standard, derivational one is proven. A derivational semantics is traditionally given by means of a set of axioms and deduction rules which define a deduction system. With such semantics, some difficulties arise when dealing with deduction rules with negative premises; also, the proof that a transition cannot take place cannot be carried out within the formal system. On the other hand, in the equational semantics approach, a transition is viewed as the application of a triadic predicate. Such a function is defined by a set of equations, and this, in a natural way, allows for the use of negative information within the system. It is shown that for Basic LOTOS, when restricted to guarded recursion, both formal reasoning systems strongly correspondSource: Fourth Workshop on Future Trends of Distributed Computing Systems, pp. 396–403, 1993
DOI: 10.1109/ftdcs.1993.344208
Metrics:
See at:
doi.org | ieeexplore.ieee.org | CNR ExploRA