Towards verified Java code generation from concurrent state machines
作者： C. Huizing , D. Bosnacki , A.J. Wijs , D. Zhang , R. Kuiper
DOI:
关键词: Concurrency 、 Programming language 、 Java 、 Real time Java 、 Modeling language 、 Finite-state machine 、 Atomicity 、 Java concurrency 、 Synchronization (computer science) 、 Computer science
摘要: We present work in progress on, verified, transformation of a modeling language based on communicating concurrent state machines, SLCO, to Java. Some concurrency related challenges, atomicity and non-standard fairness issues, are pointed out. discuss solutions Java synchronization concepts.
tue.nl 参考文章(7)
Anton Wijs, Luc Engelen, REFINER: Towards Formal Verification of Model Transformations Lecture Notes in Computer Science. pp. 258- 263 ,(2014) , 10.1007/978-3-319-06200-6_21
Jan Smans, Bart Jacobs, Frank Piessens, VeriFast for java: a tutorial Aliasing in Object-Oriented Programming. pp. 407- 442 ,(2013) , 10.1007/978-3-642-36946-9_14
Anton Wijs, Define, verify, refine : correct composition and transformation of concurrent system semantics formal aspects of component software. pp. 348- 368 ,(2013) , 10.1007/978-3-319-07602-7_21
John C. Reynolds, An Overview of Separation Logic verified software: theories, tools, experiments. pp. 460- 469 ,(2005) , 10.1007/978-3-540-69149-5_49
Anton Wijs, Luc Engelen, Efficient property preservation checking of model refinements tools and algorithms for construction and analysis of systems. pp. 565- 579 ,(2013) , 10.1007/978-3-642-36742-7_41
S Sybren Roede, Proving correctness of threaded parallel executable code generated from models described by a domain specific language Technische Universiteit Eindhoven. ,(2012)
Ljp Luc Engelen, From napkin sketches to reliable software Technische Universiteit Eindhoven. ,(2012) , 10.6100/IR740040