Formal Modeling for Magnetic Resonance Images Tamper Mitigation

The picture archiving and communication system is a medical imaging technology used primarily in healthcare organizations to store and digitally transmit electronic images and clinically-relevant reports. As demonstrated, these systems can be exploited by malicious users: in fact, considering that medical images are not digitally encrypted, any medical image modifications would be difficult to detect for a radiologist. To mitigate this aspect, in this paper a formal modelisation for picture archiving and communication system systems is proposed. The main aim is to avoid illegal writing and reading from components that should not do it, by representing the system components in terms of automa.