Как использовать Alloy для поиска ошибок в архитектуре программного обеспечения

Я получаю огромное удовольствие от изучения Alloy и рад возможности применить его в некоторых программных проектах, над которыми работаю.

В прошлом я неформально использовал облегченные формальные методы, чтобы записать в логике первого порядка некоторые из инвариантов, которые, как я ожидаю, должна иметь система. Я никогда не использовал это для поиска дефектов, а только для того, чтобы сосредоточить свой дизайн и тестирование на критических свойствах.

Сейчас я хотел бы выйти за рамки этого и использовать Alloy для поиска недостатков в архитектуре. Как я могу это сделать? Подход, который я использую, таков:

  1. Разделите архитектуру до некоторого ядра (например, удалите наборы использования вместо более сложных структур данных, используйте sig вместо более подробных перечислений)
  2. Кодируйте инвариант как assert
  3. check и run

Однако, несмотря на то, что я много узнал о Alloy, это не помогло мне улучшить мою архитектуру. В процессе упрощения моей модели кажется, что инварианты, которые я кодирую, соответственно упрощаются и сохраняются естественным образом.

Например, в архитектуре была ошибка, с которой мы столкнулись только при прототипировании и тестировании. Ошибка была связана с предположением, что если у нас есть n элемента в последовательности, мы можем разбить их на группы по m и последовательно обрабатывать каждую m-группу. (n оказывается намного больше, чем m.) Проблема, конечно, в том, что m не обязательно делит n, и поэтому последняя группа может быть слишком маленькой. Это дефект на уровне дизайна, полностью выразимый в логике, именно для этого типа дефекта и разработан Alloy. Тем не менее, моя модель из сплава не нашла его. Он просто абстрагировался от целочисленного размера (см. совет, данный в Почему Alloy сообщает мне, что 3 ›= 10? чтобы не использовать числа), разбили n на непересекающиеся группы и прекрасно заработали.

Другими словами, создается впечатление, что чтобы ваша модель содержала достаточно деталей для обнаружения дефекта, вам нужно знать о дефекте заранее.

Как вы тогда используете Alloy для проверки архитектур программного обеспечения?

PS Я понимаю, что есть много случаев, когда у вас нет этой проблемы. Например, при просмотре спецификации для распределенной системы и желании показать инварианты. Моя задача здесь заключается в том, чтобы применить Alloy для помощи в реализации, а не для проверки протокола, спецификации, конечного автомата или другой логической конструкции.


alloy
person SRobertJames    schedule 26.03.2015    source источник
comment
не могли бы вы показать свою модель сплава, которая не обнаружила ошибку? Мне любопытно, почему он не нашел (как вы его смоделировали). Я думаю, глядя на это, вы можете получить некоторое представление о том, как вам посоветовать.   -  person Bernardo Ferreira Bastos Braga    schedule 27.03.2015

Ответы (1)


arrow_upward
1
arrow_downward

Сплав не лучше всего подходит для рассуждений о числах или строках. Таким образом, ваша модель часто не может обнаружить ошибки, связанные с форматом данной строки или значением заданных целочисленных полей.

Теперь, для чего Alloy отлично подходит, так это для рассуждений об отношениях и ограничениях на эти отношения. Проверка утверждения — это один из способов убедиться в том, что заданное свойство имеет место, так что вы правы, используя исключительно этот прием, у вас может возникнуть ощущение, что вам нужно знать о дефекте заранее.

Таким образом, я предпочитаю этому подходу использование команды запуска, которая просто дает вам набор экземпляров, удовлетворяющих ограничениям вашей модели. Здесь вы сами проверите, имеет ли смысл сгенерированная серия экземпляров в контексте того, что вы моделируете. И вы, вероятно, заметите, что некоторые из ваших ограничений слишком или недостаточно ограничивают, что позволяет вам улучшить вашу модель.

person bilboul boulbil    schedule 12.05.2015