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

Question

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

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

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

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

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

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

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

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

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

Answer 1

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

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

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