975
views
0
recommends
+1 Recommend
1 collections
    0
    shares

      Studying business & IT? Drive your professional career forwards with BCS books - for a 20% discount click here: shop.bcs.org

      scite_
       
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      Zenoness detection and timed model checking for real time systems

      Published
      proceedings-article
      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
      Bookmark

            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.

            Content

            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
            1bbff1c5-71fe-4f1e-a83f-c19455919424
            © 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
            History
            Product

            1477-9358 BCS Learning & Development

            Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/VECOS2007.12
            Self URI (journal page): https://ewic.bcs.org/
            Categories
            Electronic Workshops in Computing

            Applied computer science,Computer science,Security & Cryptology,Graphics & Multimedia design,General computer science,Human-computer-interaction
            time Petri nets,zeno models,on-the-fly TCTL model checking,timed properties,real time systems,Formal methods

            Comments

            Comment on this article