An Abstraction Technique for Verifying Shared-Memory Concurrency

Modern concurrent and distributed software is highly complex. Techniques to reason about the correct behaviour of such software are essential to ensure its reliability. To be able to reason about realistic programs, these techniques must be modular and compositional as well as practical by being supported by automated tools. However, many existing approaches for concurrency verification are theoretical and focus primarily on expressivity and generality. This paper contributes a technique for verifying behavioural properties of concurrent and distributed programs that balances expressivity and usability. The key idea of the approach is that program behaviour is abstractly modelled using process algebra, and analysed separately. The main difficulty is presented by the typical abstraction gap between program implementations and their models. Our approach bridges this gap by providing a deductive technique for formally linking programs with their process-algebraic models. Our verification technique is modular and compositional, is proven sound with Coq, and has been implemented in the automated concurrency verifier VerCors. Moreover, our technique is demonstrated on multiple case studies, including the verification of a leader election protocol.

Human-Machine Interface for a Smart Wheelchair

The paper describes the integration of hardware and software with sensor technology and computer processing to develop the next generation intelligent wheelchair. The focus is a computer cluster design to test high performance computing for smart wheelchair operation and human interaction. The LabVIEW cluster is developed for real-time autonomous path planning and sensor data processing. Four small form factor computers are connected over a Gigabit Ethernet local area network to form the computer cluster. Autonomous programs are distributed across the cluster for increased task parallelism to improve processing time performance. The distributed programs operating frequency for path planning and motion control is 50Hz and 12.3Hz for 0.3 megapixel robot vision system. To monitor the operation and control of the distributed LabVIEW code, network automation is integrated into the cluster software along with a performance monitor. A link between the computer motion control program and the wheelchair joystick control of the drive train is developed for the computer control interface. A perception sensor array and control circuitry is integrated with the computer system to detect and respond to the wheelchair environment. Multiple cameras are used for image processing and scanning laser rangefinder sensors for obstacle avoidance in the cluster program. A centralized power system is integrated to power the smart wheelchair along with the cluster and sensor feedback system. The on board computer system is evaluated for cluster processing performance for the smart wheelchair, incorporating camera machine vision and LiDAR perception for terrain obstacle detection, operating in urban scenarios.