Глава
MicroTESK: A Tool for Constrained Random Test Program Generation for Microprocessors
В работе предлагается метод автоматизированного построения поведенческих моделей микропроцессоров, используемых при генерации тестовых программ для предсказания результатов их выполнения. Предложенный метод основан на использовании формальных спецификаций системы команд. Данный метод реализован в инструменте MicroTESK, разработанном в ИСП РАН. Инструмент успешно применяется для верификации промыш- ленных микропроцессоров.
This volume contains the Proceedings of 22nd Concurrency, Specification and Programming (GS&P) Workshop held on September 25-27, 2013 in Warsaw. There were 48 submissions. Each submission was reviewed by two program committee members. The committee decided to accept 40 papers. The Workshop was initiated in the mid 1970s by computer scientists and mathematicians from Warsaw and Humboldt Universities, as Polish-German annual meetings. They were suspended for some years in the 1980s and reactimed in 1992. Thereafter, the Workshop, organised alternatingly by the Institutes of Informatics and Mathematics of the University of Warsaw and the Institute of Informatics of Humboldt University in Berlin on the basis of an exchange program, has been given the name GS&P. It should be mentioned that the CS&P meetings, initially purely bilateral, since 1992 have developed into events attended by participants from a number of different countries beside Poland and Germany. The present GS&P'13 meeting attracted contributors from: Canada, Egypt, France, Germany, Italy, Nepal, The Netherlands, Poland, Russia, Serbia, Slenakia, Sweden, Turkey, United Kingdom, United States, and Vietnam. The organisation of this year's CS&P would not be possible without the resources and financing provided by seven institutions. We would like to thank the Faculty of Mathematics, Informatics and Mechanics of the University of Warsaw and the Institute of Informatics of the Humboldt University of Berlin for the continuing financial and organisational support provided to GS&P over last twenty-two years. The essential financial backing received from the Warsaw Center of Mathematics and Computer Science made the organisation of CS&P 2013 possible. Our thanks go to the Bialystok University of Technology for providing the means for publishing this proceedings volume. Last, but not the least, we are grateful for the significant financial support provided by the Vistula University in Warsaw.
Workshop on Program Semantics, Specifi cation and Verifi cation: Theory and Applications is the leading event in Russia in the fi eld of applying of the formal methods to software analysis. Proceedings of the fourth workshop are dedicated to formalisms for program semantics, formal models and veri cation, programming and speci fication languages, etc.
This volume contains the papers presented at CS&P 2014: 23th International Workshop on Concurrency, Specification and Programming held on September 28 - October 1, 2014 in Chemnitz. Since the early seventies Warsaw University and Humboldt-University have alternately organized an annual workshop - since 1993 as CS&P. Over time, it has grown from a bilateral seminar to a meeting attended also by colleagues from other countries than Poland and Germany. This year there are 34 participants from 10 countries.
Nested Petri nets is an extension of Petri net formalism with net tokens for modelling multi-agent distributed systems with complex structure. Temporal logics, such as CTL, are used to state requirements of software systems behaviour. However, in the case of nested Petri nets models, CTL is not expressive enough for specification of system behaviour. In this paper we propose an extension of CTL with a new modality for specifying agents behavior. We define syntax and formal semantics for our logic, and give small examples of its usage.