The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

I think one of an important facts to check in GUIs is that a crucial
(urgent) information (like say a temperature alarm in a nuclear plant)
is not hidden by a window displaying less important data. For instance
in an aircraft particularly nasty things happen when an alarm (visual
or sound) hides another.

P.

2017-10-10 23:03 GMT+02:00 Valentin Robert 
<valentin.robert.42 AT gmail.com>:
> Probably relevant:
> http://neutrons.uwplse.org/
>
> - Valentin
>
> On 10 October 2017 at 11:00, Daniel Schepler 
> <dschepler AT gmail.com>
>  wrote:
>>
>> On Tue, Oct 10, 2017 at 10:36 AM, Abhishek Anand
>> <abhishek.anand.iitg AT gmail.com>
>>  wrote:
>> > I am curious what you want to prove about GUIs.
>> >
>> > In the healthcare domain, I guess privacy is the biggest concern.
>>
>> I was thinking correctness of things like recommended medication
>> doses, or if it's an interface to medical equipment, then verifying
>> that certain dangerous operating conditions never happen.  A while
>> ago, somewhere on Wikipedia I read about a situation with control
>> software of a radiation therapy device.  Under a certain sequence of
>> actions that wasn't anticipated by the software designers, it could
>> end up opening all filters which was never supposed to happen,
>> resulting in a massive overdose of radiation.  (Of course, the rest of
>> what you wrote also applies here - in that particular situation, the
>> recommendation was to design hardware interlocks so that it would be
>> physically impossible for the software to accidentally leave all
>> filters open and still activate the radiation.)
>> --
>> Daniel
>
>