Blog
About

135
views
0
recommends
+1 Recommend
1 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      Modeling complex systems with VeriJ

      , , , ,

      Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2011) (VECOS)

      Verification and Evaluation of Computer and Communication Systems (VECoS 2011)

      15-16 September 2011

      VeriJ, Java, model transformation, verification, controller synthesis

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          This paper presents VeriJ, a language designed for modeling complex supervisory control problems. VeriJ is based on a subset of the Java language with some supervisory control specific constructs added; this allows to use industrial strength integrated development environments such as Eclipse to build VeriJ models and to directly use a Java debugger to execute (simulate) these models. With the aim to perform controller synthesis in a further step, VeriJ models are translated into hierarchical finite state machines (HFSM) representing the control flow graph, using modern model transformation techniques and tools. The semantics of these HFSM is then given as a pushdown system, leading to a concise and expressive representation of the underlying discrete event system. We illustrate our modeling and transformation approach with a VeriJ model of the Nim game, for which finding a winning strategy for a player can be seen as a control problem.

          Related collections

          Most cited references 7

          • Record: found
          • Abstract: not found
          • Article: not found

          The model checker SPIN

           G.J. Holzmann (1997)
            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            Nim, A Game with a Complete Mathematical Theory

              Bookmark
              • Record: found
              • Abstract: not found
              • Book Chapter: not found

              Verifying Concurrent Message-Passing C Programs with Recursive Calls

               S Chaki,  E. Clarke,  N. Kidd (2006)
                Bookmark

                Author and article information

                Contributors
                Conference
                September 2011
                September 2011
                : 1-12
                Affiliations
                Université Pierre & Marie Curie,

                CNRS-UMR 7606 (LIP6/MoVe),

                4 place Jussieu, F-75005 Paris, France
                CNRS-UMR 7606 (LIP6/MoVe) and

                Université Paris Ouest Nanterre La Défense

                200, avenue de la République, F-92001 Nanterre Cedex, France
                Article
                10.14236/ewic/VECOS2011.4
                © Yan Zhang et al. Published by BCS Learning and Development Ltd. Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2011), Tunis, Tunisia

                This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

                Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2011)
                VECOS
                5
                Tunis, Tunisia
                15-16 September 2011
                Electronic Workshops in Computing (eWiC)
                Verification and Evaluation of Computer and Communication Systems (VECoS 2011)
                Product
                Product Information: 1477-9358BCS Learning & Development
                Self URI (journal page): https://ewic.bcs.org/
                Categories
                Electronic Workshops in Computing

                Comments

                Comment on this article