2006
Journal article
Open Access
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, vol. 64, pp. 6-7
Massink M, Margaria T
Report on the 10th edition of the FMICS international workshop held in Lisbon in 2005.Source: ERCIM NEWS, vol. 64, pp. 6-7
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, vol. 261, pp. 23-42
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, vol. 261, pp. 23-42
DOI: 10.1016/j.entcs.2010.01.004
Metrics:
See at:
Electronic Notes in Theoretical Computer Science 
| CNR IRIS 
| CNR IRIS | www.sciencedirect.com
2001
Conference article
Restricted
Modeling free flight with collision avoidance.
Massink M, De Francesco N
Free jlight has been proposed as a future alternative to the current policy in Air Trafic Management (ATM) where aircraft follow predefined corridors. In free Pight pilots can choose their own optimal routes, altitudes and velocities but are also responsible for the safe and fair resolution of trajectory conjlicts. This would require a safe distributed control system were the trajectories that aircraft follow are as optimal as possible respecting suficient safety distances. In this paper we model aircraft behaviour using non-determinism in such a way that reachability analysis provides the optimal trajectories of the aircraft. We compare the obtained results with the conflict resolution solutions proposed in the literature.
Massink M, De Francesco N
Free jlight has been proposed as a future alternative to the current policy in Air Trafic Management (ATM) where aircraft follow predefined corridors. In free Pight pilots can choose their own optimal routes, altitudes and velocities but are also responsible for the safe and fair resolution of trajectory conjlicts. This would require a safe distributed control system were the trajectories that aircraft follow are as optimal as possible respecting suficient safety distances. In this paper we model aircraft behaviour using non-determinism in such a way that reachability analysis provides the optimal trajectories of the aircraft. We compare the obtained results with the conflict resolution solutions proposed in the literature.
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.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.DOI: 10.1109/qest.2007.19
Metrics:
See at:
CNR IRIS | CNR IRIS | xplorestaging.ieee.org
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
Other
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.
Massink M
In this chapter we highlight some of the more exciting recent advances and challenges in the development of model-checking technology.
See at:
CNR IRIS | ISTI Repository | CNR IRIS
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:
CNR IRIS | ISTI Repository | CNR IRIS
2002
Other
Open Access
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2005
Book
Open Access
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, 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, 2005
2007
Other
Restricted
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.
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.
2008
Other
Restricted
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.IT
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.IT
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), vol. 18 (issue 3), pp. 297-307
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), vol. 18 (issue 3), pp. 297-307
DOI: 10.1111/1467-8659.00350
Metrics:
See at:
Computer Graphics Forum | CNR IRIS | CNR IRIS | onlinelibrary.wiley.com | www.scopus.com
2009
Journal article
Restricted
Preface. International Journal on Software Tools for Technology Transfer
Margaria T, Massink M
Source: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER (PRINT), vol. 11 (issue 5), pp. 355-357
DOI: 10.1007/s10009-009-0121-6
Metrics:
Margaria T, Massink M
Source: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER (PRINT), vol. 11 (issue 5), pp. 355-357
DOI: 10.1007/s10009-009-0121-6
Metrics:
See at:
CNR IRIS | CNR IRIS | link.springer.com
2009
Book
Restricted
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)Source: ELECTRONIC COMMUNICATIONS OF THE EASST
Harrison M, Massink M
Special issue on the third international workshop on formal methods for interactive systems (FMIS 2009)Source: ELECTRONIC COMMUNICATIONS OF THE EASST
2005
Book
Restricted
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 Systems
T Margaria, M Massink
Proceedings of the Tenth International Workshop on Formal Methods for Industrial Critical Systems
2001
Book
Metadata Only Access
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 IRIS
1999
Book
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 checkingDOI: 10.1007/3-540-48234-2
Metrics:
Dams D, Gerth R, Leue S, Massink M
Theoretical and practical aspects of SPIN model checkingDOI: 10.1007/3-540-48234-2
Metrics:
See at:
doi.org | CNR IRIS | link.springer.com
2000
Conference article
Restricted
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.
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.
1997
Conference article
Restricted
Investigating the behaviour of PREMO synchronisable objects
Faconti G, Massink M
Source: EUROGRAPHICS, pp. 125-141. Granada, E, June 4-6, 1997
Faconti G, Massink M
Source: EUROGRAPHICS, pp. 125-141. Granada, E, June 4-6, 1997