Author name cluster

GianLuigi Ferrari

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

1 author row

JBHI Journal 2015 Journal Article

Automatic UPDRS Evaluation in the Sit-to-Stand Task of Parkinsonians: Kinematic Analysis and Comparative Outlook on the Leg Agility Task

Matteo Giuberti
GianLuigi Ferrari
Laura Contin
Veronica Cimolin
Corrado Azzaro
Giovanni Albani
Alessandro Mauro

In this study, we first characterize the sit-to-stand (S2S) task, which contributes to the evaluation of the degree of severity of the Parkinson's disease (PD), through kinematic features, which are then linked to the Unified Parkinson's disease rating scale (UPDRS) scores. We propose to use a single body-worn wireless inertial node placed on the chest of a patient. The experimental investigation is carried out considering 24 PD patients, comparing the obtained results directly with the kinematic characterization of the leg agility (LA) task performed by the same set of patients. We show that i) the S2S and LA tasks are rather unrelated and ii) the UPDRS distributions (for both S2S and LA tasks) across the patients have a direct impact on the observed system performance.

Details DOI

JBHI Journal 2015 Journal Article

Body-Sensor-Network-Based Kinematic Characterization and Comparative Outlook of UPDRS Scoring in Leg Agility, Sit-to-Stand, and Gait Tasks in Parkinson's Disease

Federico Parisi
GianLuigi Ferrari
Matteo Giuberti
Laura Contin
Veronica Cimolin
Corrado Azzaro
Giovanni Albani
Alessandro Mauro

Recently, we have proposed a body-sensor-network-based approach, composed of a few body-worn wireless inertial nodes, for automatic assignment of Unified Parkinson's Disease Rating Scale (UPDRS) scores in the following tasks: Leg agility (LA), Sit-to-Stand (S2S), and Gait (G). Unlike our previous works and the majority of the published studies, where UPDRS tasks were the sole focus, in this paper, we carry out a comparative investigation of the LA, S2S, and G tasks. In particular, after providing an accurate description of the features identified for the kinematic characterization of the three tasks, we comment on the correlation between the most relevant kinematic parameters and the UPDRS scoring. We analyzed the performance achieved by the automatic UPDRS scoring system and compared the estimated UPDRS evaluation with the one performed by neurologists, showing that the proposed system compares favorably with typical interrater variability. We then investigated the correlations between the UPDRS scores assigned to the various tasks by both the neurologists and the automatic system. The results, based on a limited number of subjects with Parkinson's disease (PD) (34 patients, 47 clinical trials), show poor-to-moderate correlations between the UPDRS scores of different tasks, highlighting that the patients' motor performance may vary significantly from one task to another, since different tasks relate to different aspects of the disease. An aggregate UPDRS score is also considered as a concise parameter, which can provide additional information on the overall level of the motor impairments of a Parkinson's patient. Finally, we discuss a possible implementation of a practical e-health application for the remote monitoring of PD patients.

Details DOI

TCS Journal 2005 Journal Article

Coalgebraic minimization of HD-automata for the π -calculus using polymorphic types

GianLuigi Ferrari
Ugo Montanari
Emilio Tuosto

We introduce finite-state verification techniques for the π -calculus whose design and correctness are justified coalgebraically. In particular, we formally specify and implement a minimization algorithm for HD-automata derived from π -calculus agents. The algorithm is a generalization of the partition refinement algorithm for classical automata and is specified as a coalgebraic construction defined using λ →, Π, Σ, a polymorphic λ -calculus with dependent types. The convergence of the algorithm is proved; moreover, the correspondence of the specification and the implementation is shown.

Details DOI

TCS Journal 2001 Journal Article

On the semantics of durational actions

Flavio Corradini
GianLuigi Ferrari
Marco Pistore

This paper develops a mathematical framework to describe and reason about semantic theories of processes where actions have a non-zero duration. The framework relies on the notions of reduction and observability and allows one to naturally explain the possible choices to incorporate timing information in terms of process interaction mechanisms. The framework provides a parameterized context where well-known and new theories can be formally compared and classified by a suitable instantiation of the parameters. A proof-technique to derive from the reduction semantics an equivalent SOS-based characterization is also provided.

Details DOI

I&C Journal 2000 Journal Article

Tile Formats for Located and Mobile Systems

GianLuigi Ferrari
Ugo Montanari

Standard SOS formats are limited in their ability to define the operational semantics of process calculi with concurrency, causality, and mobility, and with bound names and name generation mechanisms. In this paper we describe a general approach, based on the tile model, to the definition of the operational semantics of process calculi. By providing tile systems for located CCS and asynchronous π-calculus we demonstrate that the proposed approach is more suited than SOS to provide a uniform treatment of concurrency and mobility within a compositional framework.

Details DOI

TCS Journal 2000 Journal Article

Types for access control

Rocco De Nicola
GianLuigi Ferrari
Rosario Pugliese
Betti Venneri

KLAIM is an experimental programming language that supports a programming paradigm where both processes and data can be moved across different computing environments. This paper presents the mathematical foundations of the KLAIM type system; this system permits checking access rights violations of mobile agents. Types are used to describe the intentions (read, write, execute, …) of processes relative to the different localities with which they are willing to interact, or to which they want to migrate. Type checking then determines whether processes comply with the declared intentions, and whether they have been assigned the necessary rights to perform the intended operations at the specified localities. The KLAIM type system encompasses both subtyping and recursively defined types. The former occurs naturally when considering hierarchies of access rights, while the latter is needed to model migration of recursive processes.

Details DOI