@inproceedings{5b197c6ac3094a6b9b15f95563447122,
title = "Model checking for BPEL4WS with time",
abstract = "The mobile ambient is a formal model for mobile computation, but the real-time property of the mobility has not been well described. We extend mobile ambient with time, and then present discrete time mobile ambient calculus (DTMA). We also propose a modal logic for DTMA, and then give a model checking algorithm for DTMA on a subset of its logic formulas. Based on DTMA, we investigate the modelling and model checking for web service composition orchestration that has time constraint. Our work is a foundation for the model checking of the real-time mobile computation.",
keywords = "BPEL, Modal logic, Model checking, Timed mobile ambient",
author = "Chunming Gao and Jin Li and Zhoujun Li and Huowang Chen",
year = "2007",
doi = "10.1007/978-3-540-72909-9\_58",
language = "英语",
isbn = "9783540729082",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "528--533",
booktitle = "Advances in Web and Network Technologies, and Information Management - APWeb/WAIM 2007 International Workshops DBMAN 2007, WebETrends 2007, PAIS 2007 and ASWAN 2007, Proceedings",
address = "德国",
note = "ApWeb/WAIM 2007 International Workshops: 1st International workshop on Database Management and Applications over Networks, DBMAN 2007 - 1st Workshop on Emerging Trends of Web Technologies and Applications, WebETrends 2007 - International Workshop on ; Conference date: 16-06-2007 Through 18-06-2007",
}