Runtime Verification on Robotics Systems

Runtime verification is a technique for generating monitors from formal specification of expected behaviors for the underlying system. It can be applied to automatically evaluate system execution, either on-line or off-line, analyzing extracted execution traces; or it can be used online during operation, potentially steering the application back to a safety region if a property is violated. As a so-called light-weighted formal method, runtime verification bridges the gap between system design and implementation and shorten the distance of software quality assurance between the software testing and model checking and theorem proving. Runtime verification is considered as a highly scalable and automatic technique. Most of current runtime verification research are endeavored on the program context, in other words, on the program side and falls in the implementation level. These applications limited the benefits of runtime verification that bridges the gap among types of applications. With the proliferation of embedded systems and mobile device, dynamically verifying the firmware and mobile apps becomes a new emerging area. Due to the characteristics of runtime verification technique and limitations of the robotics systems, so far, very few research and project are located in the runtime verification on the firmware of embedded systems, which appear in most of robotics systems. Robotics systems are programmed on the firmware and only observed on device. In this paper, the authors first discussed the current runtime verifications on the embedded systems with limitations. After that, a layered runtime verification framework will be presented for the firmware verification. The case study is applied on the commonly recognized educational toolkit – LEGO Mindstorm robotics systems.

Download Full-text

On-line Tropical Epidemiology -A Case-Study from The Gambia

Methods of Information in Medicine ◽

10.1055/s-0038-1635490 ◽

1987 ◽

Vol 26 (02) ◽

pp. 73-76 ◽

Cited By ~ 3

Author(s):

Kathryn Rowan ◽

P. Byass ◽

R. W. Snow

Keyword(s):

Data Collection ◽

Field Trial ◽

Error Rates ◽

Database Management System ◽

Bed Nets ◽

Completion Rates ◽

On Line ◽

Access To Data ◽

Rapid Processing

SummaryThis paper reports on a computerised approach to the management of an epidemiological field trial, which aimed at determining the effects of insecticide-impregnated bed nets on the incidence of malaria in children. The development of a data system satisfying the requirements of the project and its implementation using a database management system are discussed. The advantages of this method of management in terms of rapid processing of and access to data from the study are described, together with the completion rates and error rates observed in data collection.

Download Full-text

RECYCLED WATER RISK PERCEPTION - A COMPARISON OF TWO CASE STUDIES

Water Practice & Technology ◽

10.2166/wpt.2007.068 ◽

2007 ◽

Vol 2 (4) ◽

Author(s):

A. Hurlimann

Keyword(s):

Risk Perception ◽

Case Studies ◽

Perceived Risk ◽

Capital City ◽

Recycled Water ◽

Urban Centre ◽

On Line ◽

Line Survey ◽

Water Uses

This paper reports results from a study comparing perceived risk associated with various recycled water uses in two Australian locations, both in the state of Victoria: the capital city Melbourne, and Bendigo a regional urban centre. Both locations are experiencing ‘drought’, but Bendigo is experiencing this in a more acute manner. A case study is used in each location. Both case studies involve future use of recycled water in new commercial buildings. An on-line survey was used to measure attitudes to recycled water of the future occupants of both buildings. The study found perceived risk associated with 11 uses of recycled water increased as the use became increasingly personal. Interestingly, no difference in perceived risk associated with 11 uses of recycled water was found between locations. Prior experience (use) of recycled water was found to be a significant and positive factor in reducing risk perception. Various attitudinal variables were found to be significant influences on perceived risk. Results indicate that reducing perceived risk of recycled water use may increase satisfaction with its use.

Download Full-text

Adventure Code Camp: Library Mobile Design in the Backcountry

Information Technology and Libraries ◽

10.6017/ital.v33i3.5480 ◽

2014 ◽

Vol 33 (3) ◽

pp. 45 ◽

Cited By ~ 2

Author(s):

David Ward ◽

James Hahn ◽

Lori Mestre

Keyword(s):

Mobile Devices ◽

Design Process ◽

Mobile Apps ◽

Library Services ◽

Mobile Web ◽

Process Outcomes ◽

Mobile Design ◽

Web App ◽

Software Services

<p>This article presents a case study exploring the use of a student Coding Camp as a bottom-up mobile design process to generate library mobile apps. A code camp sources student programmer talent and ideas for designing software services and features. This case study reviews process, outcomes, and next steps in mobile web app coding camps. It concludes by offering implications for services design beyond the local camp presented in this study. By understanding how patrons expect to integrate library services and resources into their use of mobile devices, librarians can better design the user experience for this environment.</p>

Download Full-text

On-line separation and quantification of virus antigens of different serotypes in multivalent vaccines by capillary zone electrophoresis: A case study for quality control of foot-and-mouth disease virus vaccines

Journal of Chromatography A ◽

10.1016/j.chroma.2020.461834 ◽

2021 ◽

Vol 1637 ◽

pp. 461834

Author(s):

Yanmin Song ◽

Yanli Yang ◽

Xuan Lin ◽

Qizu Zhao ◽

Zhengjun Li ◽

...

Keyword(s):

Quality Control ◽

Disease Virus ◽

Foot And Mouth Disease ◽

Mouth Disease Virus ◽

Zone Electrophoresis ◽

On Line ◽

Capillary Zone ◽

Line Separation ◽

Virus Antigens

Download Full-text

DOLARS, a Distributed On-Line Activity Recognition System by Means of Heterogeneous Sensors in Real-Life Deployments—A Case Study in the Smart Lab of The University of Almería

Sensors ◽

10.3390/s21020405 ◽

2021 ◽

Vol 21 (2) ◽

pp. 405

Author(s):

Marcos Lupión ◽

Javier Medina-Quero ◽

Juan F. Sanjuan ◽

Pilar M. Ortigosa

Keyword(s):

Real Time ◽

Activity Recognition ◽

Real Life ◽

Recognition System ◽

Machine Learning Algorithms ◽

Sensor Data ◽

Heterogeneous Sensors ◽

On Line ◽

The University

Activity Recognition (AR) is an active research topic focused on detecting human actions and behaviours in smart environments. In this work, we present the on-line activity recognition platform DOLARS (Distributed On-line Activity Recognition System) where data from heterogeneous sensors are evaluated in real time, including binary, wearable and location sensors. Different descriptors and metrics from the heterogeneous sensor data are integrated in a common feature vector whose extraction is developed by a sliding window approach under real-time conditions. DOLARS provides a distributed architecture where: (i) stages for processing data in AR are deployed in distributed nodes, (ii) temporal cache modules compute metrics which aggregate sensor data for computing feature vectors in an efficient way; (iii) publish-subscribe models are integrated both to spread data from sensors and orchestrate the nodes (communication and replication) for computing AR and (iv) machine learning algorithms are used to classify and recognize the activities. A successful case study of daily activities recognition developed in the Smart Lab of The University of Almería (UAL) is presented in this paper. Results present an encouraging performance in recognition of sequences of activities and show the need for distributed architectures to achieve real time recognition.

Download Full-text

Applying the PECSL: using case studies to demonstrate the Pedagogy of Experience Complexity for Smart Learning

Smart Learning Environments ◽

10.1186/s40561-021-00158-7 ◽

2021 ◽

Vol 8 (1) ◽

Author(s):

Pen Lister

Keyword(s):

Real World ◽

Mobile Apps ◽

Urban Environments ◽

Learning Activities ◽

Learning Activity ◽

Opportunities To Learn ◽

Practical Application ◽

Design And Development ◽

Smart Learning

AbstractThis paper discusses the uses and applications of the Pedagogy of Experience Complexity for Smart Learning (PECSL), a four-tier model of considerations for the design and development of smart learning activities. Using existing mobile apps and relevant activities as illustrative examples, the PECSL is applied to indicate concepts and mechanisms by which useful pedagogical considerations can work alongside user-centred design principles for the design and development of smart learning in urban hyper-localities. Practical application of the model is discussed using real world examples of activities as a basis to demonstrate the potential for manifold opportunities to learn, and plan for experience complexity in a smart learning activity. Case study approaches reflect on aspects of the PECSL in how it might be a useful and pragmatic guide to some of the issues faced when designing digital citizen learning activities in complex urban environments.

Download Full-text

From parametric trace slicing to rule systems

International Journal on Software Tools for Technology Transfer ◽

10.1007/s10009-021-00608-0 ◽

2021 ◽

Author(s):

Giles Reger ◽

David Rydeheard

Keyword(s):

Runtime Verification ◽

Specification Languages ◽

Execution Traces ◽

Running System ◽

Proof Of Correctness ◽

Rule Systems ◽

The Relationship ◽

Specification Techniques ◽

Previous Conference

AbstractParametric runtime verification is the process of verifying properties of execution traces of (data carrying) events produced by a running system. This paper continues our work exploring the relationship between specification techniques for parametric runtime verification. Here we consider the correspondence between trace-slicing automata-based approaches and rule systems. The main contribution is a translation from quantified automata to rule systems, which has been implemented in Scala. This then allows us to highlight the key differences in how the two formalisms handle data, an important step in our wider effort to understand the correspondence between different specification languages for parametric runtime verification. This paper extends a previous conference version of this paper with further examples, a proof of correctness, and an optimisation based on a notion of redundancy observed during the development of the translation.

Download Full-text