Radiotherapy treatments need adequate quality control (QC) to ensure a correct delivery of the prescribed dose to the target area. One of the most extended safety nets for treatments in... Show moreRadiotherapy treatments need adequate quality control (QC) to ensure a correct delivery of the prescribed dose to the target area. One of the most extended safety nets for treatments in conventional radiotherapy machines is in-vivo EPID dosimetry, which uses the dose acquired by an Electronic Portal Imaging Device (EPID) during treatment to accurately reconstruct the dose as it was delivered to the patient.We developed a method to validate radiotherapy treatments delivered on a novel system: the Unity MR-Linac. This machine, which combines a radiation source (linac) and an imaging device (MRI), will help to irradiate tumors more accurately by means of a new range of techniques only available thanks to the image guidance of the MRI during irradiation. The verification of such treatments can be performed by using images of the delivered beam captured by an EPID situated opposite to the radiation source, behind the cryostat of the MRI scanner. This project focuses on the adaptation of an already existing algorithm used with conventional linacs to the new physics and design characteristics of the Unity MR-linac. The main challenge for this adaptation is the presence of the MRI scanner between the patient and the EPID, acting as a secondary source of scatter and as an attenuation medium for the beam. Show less
Hermans, F.J.R.; Koullali, B.; Os, M.A. van; Ven, J.E.M. van der; Kazemier, B.M.; Woiski, M.D.; ... ; Triple P Grp 2017
Complex applications such as incident management, social simulations, manufacturing applications, electronic auctions, e-institutions, and business to business applications are pervasive and... Show moreComplex applications such as incident management, social simulations, manufacturing applications, electronic auctions, e-institutions, and business to business applications are pervasive and important nowadays. Agent-oriented methodology is an advance in abstractionwhich can be used by software developers to naturally model and develop systems for suchapplications. In general, with respect to design methodologies, what it may be important tostress is that control structures should be added at later stages of design, in a natural top-downmanner going from specifications to implementations, by refinement. Too much detail (be itfor the sake of efficiency) in specifications often turns out to be harmful. To paraphrase D.E.Knuth, “Premature optimization is the root of all evil” (quoted in ‘The Unix ProgrammingEnvironment’ by Kernighan and Pine, p. 91).The aim of this thesis is to adapt formal techniques to the agent-oriented methodologyinto an executable theory of refinement. The justification for doing so is to provide correctagent-based software by design. The underlying logical framework of the theory we proposeis based on rewriting logic, thus the theory is executable in the same sense as rewriting logicis. The storyline is as follows. We first motivate and explain constituting elements of agentlanguages chosen to represent both abstract and concrete levels of design. We then proposea definition of refinement between agents written in such languages. This notion of refinement ensures that concrete agents are correct with respect to the abstract ones. The advantageof the definition is that it easily leads to formulating a proof technique for refinement viathe classical notion of simulation. This makes it possible to effectively verify refinement bymodel-checking. Additionally, we propose a weakest precondition calculus as a deductivemethod based on assertions which allow to prove correctness of infinite state agents. Wegeneralise the refinement relation from single agents to multi-agent systems in order to ensure that concrete multi-agent systems refine their abstractions. We see multi-agent systemsas collections of coordinated agents, and we consider coordination artefacts as being basedeither on actions or on normative rules. We integrate these two orthogonal coordinationmechanisms within the same refinement theory extended to a timed framework. Finally, wediscuss implementation aspects. Show less
Besides the features of a class-based object-oriented language, Java integrates concurrency via its thread classes, allowing for a multithreaded flow of control. The concurrency model includes... Show moreBesides the features of a class-based object-oriented language, Java integrates concurrency via its thread classes, allowing for a multithreaded flow of control. The concurrency model includes shared-variable concurrency via instance variables, coordination via reentrant synchronization monitors, synchronous message passing, and dynamic thread creation. To reason about safety properties of multithreaded Java programs, we introduce a tool-supported assertional proof method for JavaMT ("Multi-Threaded Java"), a small sublanguage of Java, covering the mentioned concurrency issues as well as the object-based core of Java. The verification method is formulated in terms of proof-outlines, where the assertions are layered into local ones specifying the behavior of a single instance, and global ones taking care of the connections between objects. We establish the soundness and the completeness of the proof system. From an annotated program, a number of verification conditions are generated and handed over to the interactive theorem prover PVS. Show less
