@inproceedings{68f010fd0f4a41f7ab3099ca35c29745,
title = "Formalization and Verification of the PSTM Architecture",
abstract = "Python Software Transactional Memory (PSTM), was proposed to break the limiting factors which restrict diffusion of the TM paradigm into more application fields. Since the widespread use of the PSTM, it is of great significance to formally analyze and verify relevant transactional properties of this architecture. In this paper, we apply Communicating Sequential Processes (CSP) to model the PSTM. Moreover, we use the model checker Process Analysis Toolkit (PAT) to automatically simulate the developed model, and verify whether the model caters for some relevant properties, e.g. ACID. Our modeling and verification show that the PSTM can guarantee some transactional properties.",
keywords = "Formalization, PSTM, Verification",
author = "Ailun Liu and Miroslav Popovic and Huibiao Zhu",
note = "Publisher Copyright: {\textcopyright} 2017 IEEE.; 24th Asia-Pacific Software Engineering Conference, APSEC 2017 ; Conference date: 04-12-2017 Through 08-12-2017",
year = "2017",
month = jul,
day = "2",
doi = "10.1109/APSEC.2017.49",
language = "英语",
series = "Proceedings - Asia-Pacific Software Engineering Conference, APSEC",
publisher = "IEEE Computer Society",
pages = "427--435",
editor = "Jian Lv and He Zhang and Mike Hinchey and Xiao Liu",
booktitle = "Proceedings - 24th Asia-Pacific Software Engineering Conference, APSEC 2017",
address = "美国",
}