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

      Zenoness detection and timed model checking for real time systems

      1 , 1 , 2

      First International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2007) (VECOS)

      Verification and Evaluation of Computer and Communication Systems

      5-6 May 2007

      Formal methods, real time systems, time Petri nets, timed properties, on-the-fly TCTL model checking, zeno models

      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

          In this paper, we consider the time Petri net model (TPN model) and show how to detect zenoness using the state class method. Zenoness is a situation which suggests that an infinity of actions may take place in a finite amount of time. This behavior is often considered as pathological since it violates a fundamental requirement for timed systems for they cannot be infinitely fast. Models violating this property are called zeno. We state a necessary and sufficient condition for T-safe TPNs to be zeno and derive an algorithm to verify zenoness in the case of bounded TPN models. We also adapt a model checking approach to verify on-the-fly a subset of TCTL properties while taking into account zeno behaviors.

          Related collections

          Most cited references 9

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

          Symbolic Model Checking for Real-Time Systems

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

            Recoverability of Communication Protocols--Implications of a Theoretical Study

             P Merlin,  D Farber (1976)
              Bookmark
              • Record: found
              • Abstract: not found
              • Book Chapter: not found

              Timed Petri Nets and BQOs

                Bookmark

                Author and article information

                Contributors
                Conference
                May 2007
                May 2007
                : 1-15
                Affiliations
                [1 ]École Polytechnique de Montréal, Canada.

                [2 ]Univesite de Boumerdes, Algeria.

                Article
                10.14236/ewic/VECOS2007.12
                © Rachid Hadjidj et al. Published by BCS Learning and Development Ltd. First International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2007), Algiers, Algeria

                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/

                First International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2007)
                VECOS
                1
                Algiers, Algeria
                5-6 May 2007
                Electronic Workshops in Computing (eWiC)
                Verification and Evaluation of Computer and Communication Systems
                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