Description

We are considering a modern ski lift that is used to transport skiers up the mountain in Austrian Alps. A common requirement for the lift is to provide efficiency and comfort for both beginners and experienced skiers at the same time. A recently witnessed ski lift in Austria  provides this by transporting skiers with both chairs and gondolas on the same carriage line. Chairs are more efficient for experienced skiers (no taking skis off and on), while gondolas are better for beginners (no skiing skills required to get on and off the lift). Neither chairs nor gondolas are permanently attached to the fast going carriage line - the lift mechanism takes them off the line at the station, puts them through a slow motion mechanism to collect or disembark the passengers and puts them back on the line.

For the first task in the project we should consider a (model) concurrent Java implementation for such a ski lift with several sensors (e.g. carriage ID sensor) and actuators (e.g. passenger gates), proceeded by a comprehensive list of functional and safety requirements, exemplified by the following:

• the entry points for chair passengers and gondola passengers are different, thus chairs and gondolas are distributed through different slow moving paths at the station,
• the entry gates at the station should control the flow of passengers to occupy the chairs/gondolas. It is OK if a chair or gondola is not allocated with passengers, but it is not OK if there are too many passengers allocated to one such carriage,
• the chairs and gondolas should not collide on the carriage line and should maintain a safe distance between different carriages on the line,
• the station has a limited space for the temporary storage of carriages to be filled with passengers.

In the concurrent Java program such properties should be maintained by suitable synchronization classes from the Java concurrency package. The resulting model should be deadlock and data-race free.

To ensure the overall safety of the ski lift formal verification techniques can be used. In particular, the second task of the project would be to specify both data-race freeness properties and functional properties using concurrent Separation Logic for Java, following the ideas presented in [1]. This involves annotating the code developed in the first part of the project and (informal) arguing of the satisfiability of the stated properties.

Referenes

1. A. Amighi, S. Blom, M. Huisman, M. Zaharieva-Stojanovski. The VerCors Project. Setting Up Basecamp. In proceedings of Programming Languages meets Program Verification (PLPV 2012). ACM Digital Library. [PDF]
2. Clément Hurlin. Specification and Verification of Multithreaded Object-Oriented Programs with Separation Logic. PhD thesis, Université Nice - Sophia Antipolis, September 2009.
   http://tel.archives-ouvertes.fr/docs/00/42/49/79/PDF/these-clement-hurlin.pdf

Additional Resources

1. The paper
2. Project Source Code