Nasa ams java path finder12/13/2023 The utility of JPF in finding logic and timing errors is illustrated, and the remaining challenges in supporting all of RTSJ are assessed. Two examples are analyzed: jobs on a multiprogramming operating system, and a complex resource contention example involving autonomous vehicles crossing an intersection. This paper describes our implementation of an RTSJ profile (subset) in JPF, including requirements, design decisions, and current implementation status. This paper describes a translator called Java PathFinder (Jpf), from Java to Promela, the modeling language of the Spin model checker. JPF at its core is a state exploring JVM which can examine alternative paths in a Java program (e.g., via backtracking) by trying all nondeterministic choices, including thread scheduling order. Jpf is a product of a major effort by the Automated Software. The Robust Software Systems group at NASA Ames Research Center has JAVA PATHFINDER (JPF) under development, a Java model checker. Java PathFinder 2, Jpf, is a prototype translator from Java to Promela, the modeling language of the Spin model checker 4. The central features of RTSJ are real time threads user defined schedulers asynchronous events, handlers, and control transfers a priority inheritance based default scheduler non-heap memory areas such as immortal and scoped, and non-heap real time threads whose execution is not impeded by garbage collection. Model Checking Real Time Java Using Java PathFinder The Real Time Specification for Java (RTSJ) is an augmentation of Java for real time applications of various degrees of hardness.
0 Comments
Leave a Reply.AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |