[{"type":"journal_article","article_type":"original","status":"public","_id":"4468","date_updated":"2024-01-08T10:54:53Z","extern":"1","scopus_import":"1","month":"01","intvolume":" 23","abstract":[{"text":"Giotto is a high-level programming language for time-triggered control applications. The authors begin with a conceptual overview of its methodology, discuss the Giotto helicopter project, and summarize available Giotto implementations.","lang":"eng"}],"oa_version":"None","issue":"1","volume":23,"publication_identifier":{"issn":["1066-033X "]},"publication_status":"published","language":[{"iso":"eng"}],"author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"first_name":"Christoph","full_name":"Kirsch, Christoph","last_name":"Kirsch"},{"first_name":"Marco","last_name":"Sanvido","full_name":"Sanvido, Marco"},{"last_name":"Pree","full_name":"Pree, Wolfgang","first_name":"Wolfgang"}],"publist_id":"260","article_processing_charge":"No","title":"From control models to real-time code using Giotto","citation":{"ista":"Henzinger TA, Kirsch C, Sanvido M, Pree W. 2003. From control models to real-time code using Giotto. IEEE Control Systems Magazine. 23(1), 50–64.","chicago":"Henzinger, Thomas A, Christoph Kirsch, Marco Sanvido, and Wolfgang Pree. “From Control Models to Real-Time Code Using Giotto.” IEEE Control Systems Magazine. IEEE, 2003. https://doi.org/10.1109/MCS.2003.1172829.","ama":"Henzinger TA, Kirsch C, Sanvido M, Pree W. From control models to real-time code using Giotto. IEEE Control Systems Magazine. 2003;23(1):50-64. doi:10.1109/MCS.2003.1172829","apa":"Henzinger, T. A., Kirsch, C., Sanvido, M., & Pree, W. (2003). From control models to real-time code using Giotto. IEEE Control Systems Magazine. IEEE. https://doi.org/10.1109/MCS.2003.1172829","short":"T.A. Henzinger, C. Kirsch, M. Sanvido, W. Pree, IEEE Control Systems Magazine 23 (2003) 50–64.","ieee":"T. A. Henzinger, C. Kirsch, M. Sanvido, and W. Pree, “From control models to real-time code using Giotto,” IEEE Control Systems Magazine, vol. 23, no. 1. IEEE, pp. 50–64, 2003.","mla":"Henzinger, Thomas A., et al. “From Control Models to Real-Time Code Using Giotto.” IEEE Control Systems Magazine, vol. 23, no. 1, IEEE, 2003, pp. 50–64, doi:10.1109/MCS.2003.1172829."},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publisher":"IEEE","quality_controlled":"1","acknowledgement":"We thank Niklaus Wirth and Walter Schaufelberger for their advice and support of the reengineering effort of the ETH Zurich helicopter control system using Giotto. This research was supported in part by DARPA SEC grant F33615-C-98–3614, MARCO GSRC grant 98-DT-660, and AFOSR MURI grant F49620–00-1–0327. A preliminary version of this article appeared as [1].","page":"50 - 64","doi":"10.1109/MCS.2003.1172829","date_published":"2003-01-29T00:00:00Z","date_created":"2018-12-11T12:09:00Z","year":"2003","day":"29","publication":"IEEE Control Systems Magazine"},{"oa_version":"None","abstract":[{"lang":"eng","text":"Giotto is a principled, tool-supported design methodology for implementing embedded control systems on platforms of possibly distributed sensors, actuators, CPUs, and networks. Giotto is based on the principle that time-triggered task invocations plus time-triggered mode switches can form the abstract essence of programming real-time control systems. Giotto consists of a programming language with a formal semantics, and a retargetable compiler and runtime library. Giotto supports the automation of control system design by strictly separating platform-independent functionality and timing concerns from platform-dependent scheduling and communication issues. The time-triggered predictability of Giotto makes it particularly suitable for safety-critical applications with hard real-time constraints. We illustrate the platform independence and time-triggered execution of Giotto by coordinating a heterogeneous flock of Intel x86 robots and Lego Mindstorms robots."}],"month":"05","quality_controlled":"1","publisher":"Wiley-Blackwell","day":"20","language":[{"iso":"eng"}],"publication":"Software-Enabled Control: Information Technology for Dynamical Systems","publication_identifier":{"isbn":["9780471234364 "]},"year":"2003","publication_status":"published","doi":"10.1002/047172288X.ch8","date_published":"2003-05-20T00:00:00Z","date_created":"2018-12-11T12:08:59Z","page":"123 - 146","_id":"4465","status":"public","type":"book_chapter","extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2024-01-08T12:24:01Z","citation":{"apa":"Henzinger, T. A., Horowitz, B., & Kirsch, C. (2003). Embedded control systems development with Giotto. In Software-Enabled Control: Information Technology for Dynamical Systems (pp. 123–146). Wiley-Blackwell. https://doi.org/10.1002/047172288X.ch8","ama":"Henzinger TA, Horowitz B, Kirsch C. Embedded control systems development with Giotto. In: Software-Enabled Control: Information Technology for Dynamical Systems. Wiley-Blackwell; 2003:123-146. doi:10.1002/047172288X.ch8","short":"T.A. Henzinger, B. Horowitz, C. Kirsch, in:, Software-Enabled Control: Information Technology for Dynamical Systems, Wiley-Blackwell, 2003, pp. 123–146.","ieee":"T. A. Henzinger, B. Horowitz, and C. Kirsch, “Embedded control systems development with Giotto,” in Software-Enabled Control: Information Technology for Dynamical Systems, Wiley-Blackwell, 2003, pp. 123–146.","mla":"Henzinger, Thomas A., et al. “Embedded Control Systems Development with Giotto.” Software-Enabled Control: Information Technology for Dynamical Systems, Wiley-Blackwell, 2003, pp. 123–46, doi:10.1002/047172288X.ch8.","ista":"Henzinger TA, Horowitz B, Kirsch C. 2003.Embedded control systems development with Giotto. In: Software-Enabled Control: Information Technology for Dynamical Systems. , 123–146.","chicago":"Henzinger, Thomas A, Benjamin Horowitz, and Christoph Kirsch. “Embedded Control Systems Development with Giotto.” In Software-Enabled Control: Information Technology for Dynamical Systems, 123–46. Wiley-Blackwell, 2003. https://doi.org/10.1002/047172288X.ch8."},"title":"Embedded control systems development with Giotto","publist_id":"262","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"last_name":"Horowitz","full_name":"Horowitz, Benjamin","first_name":"Benjamin"},{"full_name":"Kirsch, Christoph","last_name":"Kirsch","first_name":"Christoph"}],"article_processing_charge":"No"},{"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","citation":{"ista":"Henzinger TA, Kupferman O, Majumdar R. 2003. On the universal and existential fragments of the mu-calculus. Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 2619, 49–64.","chicago":"Henzinger, Thomas A, Orna Kupferman, and Ritankar Majumdar. “On the Universal and Existential Fragments of the Mu-Calculus.” In Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , 2619:49–64. Springer, 2003. https://doi.org/10.1007/3-540-36577-X_5.","short":"T.A. Henzinger, O. Kupferman, R. Majumdar, in:, Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , Springer, 2003, pp. 49–64.","ieee":"T. A. Henzinger, O. Kupferman, and R. Majumdar, “On the universal and existential fragments of the mu-calculus,” in Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , Warsaw, Poland, 2003, vol. 2619, pp. 49–64.","ama":"Henzinger TA, Kupferman O, Majumdar R. On the universal and existential fragments of the mu-calculus. In: Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems . Vol 2619. Springer; 2003:49-64. doi:10.1007/3-540-36577-X_5","apa":"Henzinger, T. A., Kupferman, O., & Majumdar, R. (2003). On the universal and existential fragments of the mu-calculus. In Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Vol. 2619, pp. 49–64). Warsaw, Poland: Springer. https://doi.org/10.1007/3-540-36577-X_5","mla":"Henzinger, Thomas A., et al. “On the Universal and Existential Fragments of the Mu-Calculus.” Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , vol. 2619, Springer, 2003, pp. 49–64, doi:10.1007/3-540-36577-X_5."},"title":"On the universal and existential fragments of the mu-calculus","article_processing_charge":"No","publist_id":"263","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"first_name":"Orna","full_name":"Kupferman, Orna","last_name":"Kupferman"},{"last_name":"Majumdar","full_name":"Majumdar, Ritankar","first_name":"Ritankar"}],"publication":"Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ","day":"14","year":"2003","date_created":"2018-12-11T12:08:59Z","date_published":"2003-03-14T00:00:00Z","doi":"10.1007/3-540-36577-X_5","page":"49 - 64","acknowledgement":"This work was supported in part by NSF grant CCR-9988172, the AFOSR MURI grant F49620-00-1-0327, and a Microsoft Research Fellowship.","publisher":"Springer","quality_controlled":"1","extern":"1","date_updated":"2024-01-08T13:17:35Z","_id":"4466","status":"public","conference":{"start_date":"2003-04-07","location":"Warsaw, Poland","end_date":"2003-04-11","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"type":"conference","language":[{"iso":"eng"}],"publication_status":"published","publication_identifier":{"isbn":["9783540008989"]},"volume":2619,"oa_version":"None","abstract":[{"text":"One source of complexity in the μ-calculus is its ability to specify an unbounded number of switches between universal (AX) and existential (EX) branching modes. We therefore study the problems of satisfiability, validity, model checking, and implication for the universal and existential fragments of the μ-calculus, in which only one branching mode is allowed. The universal fragment is rich enough to express most specifications of interest, and therefore improved algorithms are of practical importance. We show that while the satisfiability and validity problems become indeed simpler for the existential and universal fragments, this is, unfortunately, not the case for model checking and implication. We also show the corresponding results for the alternationfree fragment of the μ-calculus, where no alternations between least and greatest fixed points are allowed. Our results imply that efforts to find a polynomial-time model-checking algorithm for the μ-calculus can be replaced by efforts to find such an algorithm for the universal or existential fragment.","lang":"eng"}],"intvolume":" 2619","month":"03","alternative_title":["LNCS"]},{"citation":{"mla":"Henzinger, Thomas A., et al. “Software Verification with BLAST.” Proceedings of the 10th International SPIN Workshop , vol. 2648, Springer, 2003, pp. 235–39, doi:10.1007/3-540-44829-2_17.","apa":"Henzinger, T. A., Jhala, R., Majumdar, R., & Sutre, G. (2003). Software verification with BLAST. In Proceedings of the 10th International SPIN Workshop (Vol. 2648, pp. 235–239). Portland, OR, USA: Springer. https://doi.org/10.1007/3-540-44829-2_17","ama":"Henzinger TA, Jhala R, Majumdar R, Sutre G. Software verification with BLAST. In: Proceedings of the 10th International SPIN Workshop . Vol 2648. Springer; 2003:235-239. doi:10.1007/3-540-44829-2_17","ieee":"T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, “Software verification with BLAST,” in Proceedings of the 10th International SPIN Workshop , Portland, OR, USA, 2003, vol. 2648, pp. 235–239.","short":"T.A. Henzinger, R. Jhala, R. Majumdar, G. Sutre, in:, Proceedings of the 10th International SPIN Workshop , Springer, 2003, pp. 235–239.","chicago":"Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Grégoire Sutre. “Software Verification with BLAST.” In Proceedings of the 10th International SPIN Workshop , 2648:235–39. Springer, 2003. https://doi.org/10.1007/3-540-44829-2_17.","ista":"Henzinger TA, Jhala R, Majumdar R, Sutre G. 2003. Software verification with BLAST. Proceedings of the 10th International SPIN Workshop . SPIN: Model Checking Software, LNCS, vol. 2648, 235–239."},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","publist_id":"264","author":[{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jhala, Ranjit","last_name":"Jhala","first_name":"Ranjit"},{"last_name":"Majumdar","full_name":"Majumdar, Ritankar","first_name":"Ritankar"},{"first_name":"Grégoire","last_name":"Sutre","full_name":"Sutre, Grégoire"}],"title":"Software verification with BLAST","acknowledgement":"This work was supported in part by the NSF grants CCR-0085949 and CCR-9988172, the DARPA PCES grant F33615-00-C-1693, the MARCO GSRC grant 98-DT-660, and a Microsoft Research Fellowship.","quality_controlled":"1","publisher":"Springer","year":"2003","publication":"Proceedings of the 10th International SPIN Workshop ","day":"28","page":"235 - 239","date_created":"2018-12-11T12:09:00Z","date_published":"2003-04-28T00:00:00Z","doi":"10.1007/3-540-44829-2_17","_id":"4467","conference":{"name":"SPIN: Model Checking Software","end_date":"2003-05-10","location":"Portland, OR, USA","start_date":"2003-05-09"},"type":"conference","status":"public","date_updated":"2024-01-08T14:05:29Z","extern":"1","abstract":[{"lang":"eng","text":"BLAST (the Berkeley Lazy Abstraction Software verification Tool) is a verification system for checking safety properties of C programs using automatic property-driven construction and model checking of software abstractions. Blast implements an abstract-model check-refine loop to check for reachability of a specified label in the program. The abstract model is built on the fly using predicate abstraction. This model is then checked for reachability. If there is no (abstract) path to the specified error label, Blast reports that the system is safe and produces a succinct proof. Otherwise, it checks if the path is feasible using symbolic execution of the program. If the path is feasible, Blast outputs the path as an error trace, otherwise, it uses the infeasibility of the path to refine the abstract model. Blast short-circuits the loop from abstraction to verification to refinement, integrating the three steps tightly through “lazy abstraction” [5]. This integration can offer significant advantages in performance by avoiding the repetition of work from one iteration of the loop to the next. "}],"oa_version":"None","alternative_title":["LNCS"],"scopus_import":"1","intvolume":" 2648","month":"04","publication_status":"published","publication_identifier":{"isbn":["9783540401179"]},"language":[{"iso":"eng"}],"volume":2648},{"type":"conference","conference":{"name":"CAV: Computer Aided Verification","end_date":"2003-07-12","location":"Boulder, CO, USA","start_date":"2003-07-08"},"status":"public","_id":"4463","date_updated":"2024-01-10T11:05:53Z","extern":"1","alternative_title":["LNCS"],"month":"06","intvolume":" 2725","abstract":[{"lang":"eng","text":"We present an algorithm called TAR (“Thread-modular Abstraction Refinement”) for model checking safety properties of concurrent software. The TAR algorithm uses thread-modular assume-guarantee reasoning to overcome the exponential complexity in the control state of multithreaded programs. Thread modularity means that TAR explores the state space of one thread at a time, making assumptions about how the environment can interfere. The TAR algorithm uses counterexample-guided predicate-abstraction refinement to overcome the usually infinite complexity in the data state of C programs. A successive approximation scheme automatically infers the necessary precision on data variables as well as suitable environment assumptions. The scheme is novel in that transition relations are approximated from above, while at the same time environment assumptions are approximated from below. In our software verification tool BLAST we have implemented a fully automatic race checker for multithreaded C programs which is based on the TAR algorithm. This tool has verified a wide variety of commonly used locking idioms, including locking schemes that are not amenable to existing dynamic and static race checkers such as ERASER or WARLOCK."}],"oa_version":"None","volume":2725,"publication_identifier":{"isbn":["9783540405245"]},"publication_status":"published","language":[{"iso":"eng"}],"publist_id":"266","author":[{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Ranjit","full_name":"Jhala, Ranjit","last_name":"Jhala"},{"last_name":"Majumdar","full_name":"Majumdar, Ritankar","first_name":"Ritankar"},{"last_name":"Qadeer","full_name":"Qadeer, Shaz","first_name":"Shaz"}],"article_processing_charge":"No","title":"Thread-modular abstraction refinement","citation":{"mla":"Henzinger, Thomas A., et al. “Thread-Modular Abstraction Refinement.” Proceedings of the 15th International Conference on Computer Aided Verification, vol. 2725, Springer, 2003, pp. 262–74, doi:10.1007/978-3-540-45069-6_27.","short":"T.A. Henzinger, R. Jhala, R. Majumdar, S. Qadeer, in:, Proceedings of the 15th International Conference on Computer Aided Verification, Springer, 2003, pp. 262–274.","ieee":"T. A. Henzinger, R. Jhala, R. Majumdar, and S. Qadeer, “Thread-modular abstraction refinement,” in Proceedings of the 15th International Conference on Computer Aided Verification, Boulder, CO, USA, 2003, vol. 2725, pp. 262–274.","apa":"Henzinger, T. A., Jhala, R., Majumdar, R., & Qadeer, S. (2003). Thread-modular abstraction refinement. In Proceedings of the 15th International Conference on Computer Aided Verification (Vol. 2725, pp. 262–274). Boulder, CO, USA: Springer. https://doi.org/10.1007/978-3-540-45069-6_27","ama":"Henzinger TA, Jhala R, Majumdar R, Qadeer S. Thread-modular abstraction refinement. In: Proceedings of the 15th International Conference on Computer Aided Verification. Vol 2725. Springer; 2003:262-274. doi:10.1007/978-3-540-45069-6_27","chicago":"Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Shaz Qadeer. “Thread-Modular Abstraction Refinement.” In Proceedings of the 15th International Conference on Computer Aided Verification, 2725:262–74. Springer, 2003. https://doi.org/10.1007/978-3-540-45069-6_27.","ista":"Henzinger TA, Jhala R, Majumdar R, Qadeer S. 2003. Thread-modular abstraction refinement. Proceedings of the 15th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 2725, 262–274."},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","quality_controlled":"1","publisher":"Springer","acknowledgement":"This work was supported in part by the NSF grants CCR-0085949 and CCR-0234690, the DARPA grant F33615-00-C-1693, and the MARCO grant 98-DT-660.","page":"262 - 274","date_published":"2003-06-27T00:00:00Z","doi":"10.1007/978-3-540-45069-6_27","date_created":"2018-12-11T12:08:59Z","year":"2003","day":"27","publication":"Proceedings of the 15th International Conference on Computer Aided Verification"}]