Hello, I am Meryem Afendi, a Phd Student at Paris-Est Créteil University. My Phd thesis is about formal verification of Cyber Physical Systems (CPSs) using the formal method Event-B [1] and its support tool Rodin [2,3]. Rodin is an Eclipse-based IDE that allows modelling and verifying systems in Event-B. Once an Event-B model is specified and syntactically checked in the Rodin Platform, a set of proof obligations is generated by the proof obligation generator of the Rodin platform. ThesePOs need to be proved in order to ensure the correctness of developments and refinements. They can be proved automatically or interactively using the set of provers, like predicate provers and SMT solvers as well as external provers.
Currently I am working on interfacing the computer algebra system SageMath with the Rodin platform to treat continuous aspects of Cyber-Physical Systems in Event-B. The continuous aspects of CPSs are generally represented by ordinary differential equations. Our goal is to extract a given differential equation from Rodin, send it to SageMath and then recover the result in Rodin. Therefore, I would like to learn: -> how can we communicate with SageMath using JAVA in order to send the parameters of a given differential equation to the "desolve" function for example. -> To solve a differential equation using SageMath, we need to define each variable separately. How can we automate this without the need to define the same variables each time SageMath is called. -> Can we send a command script to SageMath. -> Can we save the result returned by SageMath in a text file to use it in Rodin. [1] Jean-Raymond Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York, NY, USA, 1st edition, 2010. [2] Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Thái Son Hoàng, Farhad Mehta, and Laurent Voisin. Rodin: an open toolset for modelling and reasoning in Event-B. International Journal on Software Tools for Technology Transfer, 12(6):447–466, 2010. [3] Rodin. User Manual of the RODIN Platform, October 2007. http://deployeprints.ecs.soton.ac.uk/11/1/manual-2.3.pdf. I would like to thank you for your help. If you need more details, don’t hesitate to contact me. Best regards, Meryem Afendi -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/62e4569c-08a7-4b12-903e-f2b4eeed8f0cn%40googlegroups.com.
