ACM Portal
  Subscribe (Full Service)    Register (Limited Service, Free)    Login
  Search:   The ACM Digital Library   The Guide
  
ACM Home Page
Please provide us with feedback. Feedback
Digital Library logoTake a look at the new version of this page: [ beta version ]. Tell us what you think.
Automata for modeling real-time systems
Source Proceedings of the seventeenth international colloquium on Automata, languages and programming table of contents
Warwick University, England
Pages: 322 - 335  
Year of Publication: 1990
ISBN:0-387-52826-1
Authors
Rajeev Alur
D. L. Dill
Publisher
Springer-Verlag New York, Inc.  New York, NY, USA
Bibliometrics
Downloads (6 Weeks): n/a,   Downloads (12 Months): n/a,   Citation Count: 41
Additional Information:

cited by   index terms   collaborative colleagues  

Tools and Actions: Review this Article  

CITED BY  41
Victor A. Braberman , Miguel Felder, Verification of real-time designs: combining scheduling theory with automatic formal verification, ACM SIGSOFT Software Engineering Notes, v.24 n.6, p.494-510, Nov. 1999
Kristina Lundqvist , Lars Asplund, A formal model of the Ada Ravenscar tasking profile; delay until, ACM SIGAda Ada Letters, v.XIX n.3, p.15-21, Sept. 1999
Manfred Broy, Functional specification of time-sensitive communicating systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.2 n.1, p.1-46, Jan. 1993
Adnan Aziz , Felice Balarin , Robert Brayton , Alberto Sangiovanni-Vincentelli, Sequential synthesis using S1S, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.612-617, November 05-09, 1995, San Jose, California, United States
Patricia Bouyer, A logical characterization of data languages, Information Processing Letters, v.84 n.2, p.75-85, 31 October 2002
Jan Chomicki, Real-time integrity constraints, Proceedings of the eleventh ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.274-282, June 02-05, 1992, San Diego, California, United States
James C. Corbett, Constructing abstract models of concurrent real-time software, ACM SIGSOFT Software Engineering Notes, v.21 n.3, p.250-260, May 1996
R. P. Kurshan, The complexity of verification, Proceedings of the twenty-sixth annual ACM symposium on Theory of computing, p.365-371, May 23-25, 1994, Montreal, Quebec, Canada
Felice Balarin, Worst-case analysis of discrete systems, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.347-353, November 07-11, 1999, San Jose, California, United States
Robyn R. Lutz , Johnny S. K. Wong, Detecting Unsafe Error Recovery Schedules, IEEE Transactions on Software Engineering, v.18 n.8, p.749-760, August 1992
Zhiming Liu , Mathai Joseph, Specification and verification of fault-tolerance, timing, and scheduling, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.1, p.46-89, Jan. 1999
Felice Balarin, Worst-case analysis of discrete systems based on conditional abstractions, Proceedings of the seventh international workshop on Hardware/software codesign, p.115-119, March 1999, Rome, Italy
Rajeev Alur , Tomás Feder , Thomas A. Henzinger, The benefits of relaxing punctuality, Proceedings of the tenth annual ACM symposium on Principles of distributed computing, p.139-152, August 19-21, 1991, Montreal, Quebec, Canada
Victor A. Braberman, Automatic verification of real-time designs, Proceedings of the 21st international conference on Software engineering, p.716-717, May 16-22, 1999, Los Angeles, California, United States
Felice Balarin , Alberto L. Sangiovanni-Vincentelli, Iterative algorithms for formal verification of embedded real-time systems, Proceedings of the 1994 IEEE/ACM international conference on Computer-aided design, p.450-457, November 06-10, 1994, San Jose, California, United States
V. Chandramouli , J. P. Whittemore , K. A. Sakallah, AFTA: a formal delay model for functional thinking analysis, Proceedings of the conference on Design, automation and test in Europe, p.350-355, February 23-26, 1998, Le Palais des Congrés de Paris, France
Enrico Vicario, Static Analysis and Dynamic Steering of Time-Dependent Systems, IEEE Transactions on Software Engineering, v.27 n.8, p.728-748, August 2001
Stephen Edwards , Luciano Lavagno , Edward A. Lee , Alberto Sangiovanni-Vincentelli, Design of embedded systems: formal models, validation, and synthesis, Readings in hardware/software co-design, Kluwer Academic Publishers, Norwell, MA, 2001
Rajeev Alur , Thomas A. Henzinger , Moshe Y. Vardi, Parametric real-time reasoning, Proceedings of the twenty-fifth annual ACM symposium on Theory of computing, p.592-601, May 16-18, 1993, San Diego, California, United States
Farn Wang, Parametric Analysis of Computer Systems, Formal Methods in System Design, v.17 n.1, p.39-60, Aug. 2000
Abdeslam En-Nouaary , Rachida Dssouli , Ferhat Khendek, Timed Wp-Method: Testing Real-Time Systems, IEEE Transactions on Software Engineering, v.28 n.11, p.1023-1038, November 2002
L. E. Moser , Y. S. Ramakrishna , G. Kutty , P. M. Melliar-Smith , L. K. Dillon, A graphical environment for the design of concurrent real-time systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.6 n.1, p.31-79, Jan. 1997
Patricia Bouyer, Forward Analysis of Updatable Timed Automata, Formal Methods in System Design, v.24 n.3, p.281-320, May 2004
Giacomo Bucci , Enrico Vicario, Compositional Validation of Time-Critical Systems Using Communicating Time Petri Nets, IEEE Transactions on Software Engineering, v.21 n.12, p.969-992, December 1995
Edmund M. Clarke , Bernd-Holger Schlingloff, Model checking, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
A. Burns, How to Verify a Safe Real-Time System: The Application of Model Checking and Timed Automata to the Production Cell Case Study, Real-Time Systems, v.24 n.2, p.135-151, March 2003
Sérgio Campos , Edmund M. Clarke , Orna Grumberg, Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System, Formal Methods in System Design, v.17 n.2, p.163-192, Oct. 2000
Stavros Tripakis , Sergio Yovine, Analysis of Timed Systems Using Time-Abstracting Bisimulations, Formal Methods in System Design, v.18 n.1, p.25-68, January.2001
Atanas Marinov Atanassov, Approach for software realization of processor for real time control model of photometric systems complex, Proceedings of the 4th international conference conference on Computer systems and technologies: e-Learning, p.327-332, June 19-20, 2003, Rousse, Bulgaria
James C. Corbett, Timing Analysis of Ada Tasking Programs, IEEE Transactions on Software Engineering, v.22 n.7, p.461-483, July 1996
Patricia Bouyer , Catherine Dufourd , Emmanuel Fleury , Antoine Petit, Updatable timed automata, Theoretical Computer Science, v.321 n.2-3, p.291-345, 16 August 2004
Jordi Cortadella , Michael Kishinevsky , Luciano Lavagno , Alexandre Yakovlev, Deriving Petri Nets from Finite Transition Systems, IEEE Transactions on Computers, v.47 n.8, p.859-882, August 1998
Jens Chr. Godskesen , Kim G. Larsen, Synthesizing distinguishing formulae for real time systems, Nordic Journal of Computing, v.2 n.3, p.338-357, Fall 1995
Patricia Bouyer , Antoine Petit, A Kleene/Büchi-like theorem for clock languages, Journal of Automata, Languages and Combinatorics, v.7 n.2, p.167-186, November 2001
Nancy A. Lynch , Hagit Attiya, Using mappings to prove timing properties, Distributed Computing, v.6 n.2, p.121-139, September 1992
Kim G. Larsen , Justin Pearson , Carsten Weise , Wang Yi, Clock difference diagrams, Nordic Journal of Computing, v.6 n.3, p.271-298, Fall 1999
Feng Lin, Theorem of abstraction for equivalent controllers in hybrid systems, Information Sciences—Informatics and Computer Science: An International Journal, v.173 n.1-3, p.181-195, 16 June 2005
Hanifa Boucheneb , Rachid Hadjidj, CTL* model checking for time Petri nets, Theoretical Computer Science, v.353 n.1, p.208-227, 14 March 2006
Thomas Watteyne , Isabelle Augé-Blum , Stéphane Ubéda, Dual-mode real-time MAC protocol for wireless sensor networks: a validation/simulation approach, Proceedings of the first international conference on Integrated internet ad hoc and sensor networks, May 30-31, 2006, Nice, France
S. Di Gennaro , C. Horn , S. R. Kulkarni , P. J. Ramadge, Reduction of Timed Hybrid Systems, Discrete Event Dynamic Systems, v.8 n.4, p.343-351, December 1998
Hesham Saadawi , Gabriel Wainer, Verification of real-time DEVS models, Proceedings of the 2009 Spring Simulation Multiconference, March 22-27, 2009, San Diego, California

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming


General Terms:
Languages, Theory, Verification

Collaborative Colleagues:
Rajeev Alur: colleagues
D. L. Dill: colleagues

The ACM Portal is published by the Association for Computing Machinery. Copyright © 2010 ACM, Inc.
Terms of Usage   Privacy Policy   Code of Ethics   Contact Us

Useful downloads: Adobe Acrobat    QuickTime    Windows Media Player    Real Player