Formal and model driven design of the bright light therapy system Luxamet

FAUST, Oliver and YU, Wenwei (2015). Formal and model driven design of the bright light therapy system Luxamet. Journal of Mechanics in Medicine and Biology, 16 (05), p. 1650065.

[img]
Preview
PDF
LUXAMET.pdf - Submitted Version
All rights reserved.

Download (370kB) | Preview
Official URL: http://www.worldscientific.com/doi/abs/10.1142/S02...
Link to published version:: https://doi.org/10.1142/S0219519416500652
Related URLs:

    Abstract

    Seasonal depression seriously diminishes the quality of life for many patients. To improve their condition, we propose LUXAMET, a bright light therapy system. This system has the potential to relieve patients from some of the symptoms caused by seasonal depression. The system was designed with a formal and model driven design methodology. This methodology enabled us to minimize systemic hazards, like blinding patients with an unhealthy dose of light. This was achieved by controlling race conditions and memory leaks, during design time. We prove that the system specification is deadlock as well as livelock free and there are no invariant violations. These proofs, together with the similarity between specification model and implementation code, make us confident that the implemented system is a reliable tool which can help patients during seasonal depression.

    Item Type: Article
    Identification Number: https://doi.org/10.1142/S0219519416500652
    Page Range: p. 1650065
    Depositing User: Oliver Faust
    Date Deposited: 31 Jul 2017 10:24
    Last Modified: 08 Jul 2019 18:30
    URI: http://shura.shu.ac.uk/id/eprint/11455

    Actions (login required)

    View Item View Item

    Downloads

    Downloads per month over past year

    View more statistics