The Theory of Timed I/O Automata (eBook, PDF)

Sofort per Download lieferbar

25,95 €

inkl. MwSt.

Jetzt bewerten

Alle Infos zum eBook verschenken

PAYBACK Punkte

13 °P sammeln!

This monograph presents the timed input/output automaton (TIOA) modeling framework, a basic mathematical framework to support description and analysis of timed (computing) systems. Timed systems are systems in which desirable correctness or performance properties of the system depend on the timing of events, not just on the order of their occurrence. Timed systems are employed in a wide range of domains including communications, embedded systems, real-time operating systems, and automated control. Many applications involving timed systems have strong safety, reliability, and predictability req...

Weiterlesen / Aufklappen

Dieser Download kann aus rechtlichen Gründen nur mit Rechnungsadresse in A, B, BG, CY, CZ, D, DK, EW, E, FIN, F, GR, HR, H, IRL, I, LT, L, LR, M, NL, PL, P, R, S, SLO, SK ausgeliefert werden.

Dilsun Kaynar is a postdoctoral researcher at CyLab, Carnegie Mellon University. Previously, she was a postdoctoral research associate in the Theory of Distributed Systems Group at MIT's Computer Science and Artificial Intelligence Laboratory. She received her PhD degree from the University of Edinburgh at the Laboratory for Foundations of Computer Science and her BSc in Computer Engineering from METU in Turkey. The broad area of her research is the specification, programming, and verification of distributed computing systems. Her PhD work focused on the design of functional programming languages that support mobile computation. She investigated the application of type-based analysis in this context, in particular to improve safety and security of systems. In her postdoctoral research at MIT, she worked on the development of I/O automata-based formal modeling frameworks for distributed systems, with collaborators including Nancy Lynch, Roberto Segala, and Frits Vaandrager. She is currently pursuing research at CMU CyLab, developing methods for analyzing security guarantees offered by contemporary secure systems and establishing foundations for data privacy, based on specializations of general formal frameworks for distributed computing such as I/O automata. Dilsun Kaynar is a postdoctoral researcher at CyLab, Carnegie Mellon University. Previously, she was a postdoctoral research associate in the Theory of Distributed Systems Group at MIT's Computer Science and Artificial Intelligence Laboratory. She received her PhD degree from the University of Edinburgh at the Laboratory for Foundations of Computer Science and her BSc in Computer Engineering from METU in Turkey. The broad area of her research is the specification, programming, and verification of distributed computing systems. Her PhD work focused on the design of functional programming languages that support mobile computation. She investigated the application of type-based analysis in this context, in particular to improve safety and security of systems. In her postdoctoral research at MIT, she worked on the development of I/O automata-based formal modeling frameworks for distributed systems, with collaborators including Nancy Lynch, Roberto Segala, and Frits Vaandrager. She is currently pursuing research at CMU CyLab, developing methods for analyzing security guarantees offered by contemporary secure systems and establishing foundations for data privacy, based on specializations of general formal frameworks for distributed computing such as I/O automata. Roberto Segala is a Professor at the University of Verona, Italy, and heads the Formal Models and Verification group at the Department of Computer Science. Prior to joining the University of Verona in 2001,he was research associate at the University of Bologna.He received his Laurea in Computer Science from the University of Pisa as a student of the Scuola Normale Superiore, and his Masters and PhD in Computer Science from MIT. As part of his PhD work, he made contributions to the theory of liveness and receptiveness for real-time systems and he designed the model of Probabilistic Automata for the formal analysis of randomized distributed algorithms. After that, he worked with Lynch, Kaynar, Vaandrager and others on the hybrid extension of the I/O automata framework. He also worked on model checking of probabilistic real-time systems, contributing to the design of some of the algorithms used in the PRISM model checker. One of his long-term goals is to design a general mathematical model that can be used for the description and analysis of systems that exhibit stochastic hybrid behavior. Roberto Segala is a Professor at the University of Verona, Italy, and heads the Formal Models and Verification group at the Department of Computer Science. Prior to joining the University of Verona in 2001,he was research associate at the University of Bologna.He received his Laurea in Computer Science from the University of Pisa as a student of the Scuola Normale Superiore, and his Masters and PhD in Computer Science from MIT. As part of his PhD work, he made contributions to the theory of liveness and receptiveness for real-time systems and he designed the model of Probabilistic Automata for the formal analysis of randomized distributed algorithms. After that, he worked with Lynch, Kaynar, Vaandrager and others on the hybrid extension of the I/O automata framework. He also worked on model checking of probabilistic real-time systems, contributing to the design of some of the algorithms used in the PRISM model checker. One of his long-term goals is to design a general mathematical model that can be used for the description and analysis of systems that exhibit stochastic hybrid behavior.