Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Голландский американский компьютерный ученый Джерард Дж. Холцманн (род. 1951) - голландский американский компьютерный ученый и исследователь в лабораториях Белл и НАСА, наиболее известный как разработчик проверки модели SPIN.
Dutch American computer scientist
Gerard J. Holzmann (born 1951) is a Dutch American computer scientist and researcher at Bell Labs and NASA, best known as the developer of the SPIN model checker.
Биография
Холцманн родился в Амстердаме, Нидерланды, и получил степень инженера в области электротехники в Технологическом университете Делфта в 1976 году. Впоследствии он также получил степень доктора философии в университете Делфта в 1979 году под руководством Виллема ван дер Поэля и Дж. Л. де Кроеса с диссертацией под названием "Проблемы координации в многопроцессорных системах". После получения стипендии Фулбрайта он был аспирантом в Университете Южной Калифорнии еще один год, где работал с Пер Бринч Хансеном. В 1980 году он начал работать в Bell Labs в Мюррей-Хилл в течение года. В Нидерландах он был ассистентом профессора в Технологическом университете Делфта в течение двух лет. В 1983 году он вернулся в Bell Labs, где работал в Центре исследований в области вычислительной науки (бывшая исследовательская группа Unix). В 2003 году он присоединился к NASA, где возглавляет лабораторию NASA JPL по надежному программному обеспечению в Пасадене, Калифорния, и является членом JPL. В 2005 году он был выбран на премию "Теория и практика" Парижа Канелакиса. В 2011 году он был принят в качестве члена Ассоциации вычислительной техники. В октябре 2012 года он был награжден медалью НАСА за выдающиеся инженерные достижения.
Holzmann was born in Amsterdam, Netherlands and received an Engineer's degree in electrical engineering from the Delft University of Technology in 1976. He subsequently also received his PhD degree from Delft University in 1979 under Willem van der Poel and J. L. de Kroes with a thesis entitled Coordination problems in multiprocessing systems. After receiving a Fulbright Scholarship he was a post graduate student at the University of Southern California for another year, where he worked with Per Brinch Hansen. In 1980 he started at Bell Labs in Murray Hill for a year. Back in the Netherlands he was assistant professor at the Delft University of Technology for two years. In 1983 he returned to Bell Labs where he worked in the Computing Science Research Center (the former Unix research group). In 2003 he joined NASA, where he leads the NASA JPL Laboratory for Reliable Software in Pasadena, California and is a JPL fellow. He was selected for the Paris Kanellakis Theory and Practice Award in 2005. In 2011 he was inducted as a Fellow of the Association for Computing Machinery. He was awarded the NASA Exceptional Engineering Achievement Medal in October 2012.
Работа
Холцманн известен разработкой проверки модели SPIN (SPIN - сокращение от Simple Promela Interpreter) в 1980-х годах в Bell Labs. Это устройство может проверять правильность одновременного программного обеспечения, с 1991 года свободно доступного.
Holzmann is known for the development of the SPIN model checker (SPIN is short for Simple Promela Interpreter) in the 1980s at Bell Labs. This device can verify the correctness of concurrent software, since 1991 freely available.