VERIFICATION OF USER INTERFACE DISTRIBUTION BASED ON Π-CALCULUS
Abstract and keywords
Abstract (English):
Opisan metod verifikacii raspredeleniya pol'zovatel'skogo interfeysa, v osnove kotorogo lezhit matematicheskiy apparat pi-ischisleniya. Razrabotany pravila i procedura raspredeleniya elementov interfeysa po otdel'nym ustroystvam. Privedeno poshagovoe opisanie verifikacii raspredeleniya interfeysa po razrabotannym pravi-lam v terminah pi-ischisleniya.

Keywords:
verifikaciya, formalizaciya, raspredelenie, raspredelennyy interfeys, pol'zovatel'skiy interfeys, pi-ischislenie, redukciya
Text
Text (PDF): Read Download

Введение        

         Распределенные пользовательские интерфейсы (РПИ) подразумевают работу пользователя с приложением посредством нескольких устройств одновременно, что повышает функциональность, продуктивность и удобство использования приложения [1]. В настоящее время существуют следующие реализации РПИ: система синхронизации смартфона с часами; система управления устройствами с помощью телефона или планшета; РПИ для совместного принятия решений и другие. Для проектирования нового РПИ необходимо всякий раз разрабатывать логику распределения элементов интерфейса. Такая ситуация затрудняет массовое внедрение РПИ ввиду непонимания пользователями логики распределения и нежелания испытывать когнитивную нагрузку, связанную с освоением новых интерфейсов [2], а также относительно большими трудозатратами разработчиков. Кроме того, сложность распределения элементов РПИ растет экспоненциально. В частности, для распределения интерфейса, состоящего из двух элементов, на два устройства необходимо рассмотреть девять возможных вариантов распределения, поскольку один элемент РПИ может быть распределен на одно из двух устройств или сразу на оба.

         Элементы РПИ используются в ситуационных центрах. В этих центрах экраны коллективного пользования отображают графики, видеоизображения и другие формы графического представления информации. Главной задачей при проектировании ситуационных центров является компоновка устройств и определение форм представления информации таким образом, чтобы минимизировать время принятия решения. Распределение информации по экранам центра производит оператор [3; 4] с учетом требований эргономики [5].

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

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

1. Правила распределения элементов интерфейса

К типовым структурным блокам интерфейса относятся основной блок , заголовок , подвал , левая колонка  и правая колонка  [6]. Рассмотрим в качестве примера распределение упрощенного интерфейса интернет-магазина (рис. 1). Этот интерфейс содержит структурные блоки , логические блоки  и элементы .

Первоначально исходный интерфейс отображается на устройстве (рис. 2). Распределенный интерфейс  располагается на основном и вспомогательном  устройствах.  Вершинами графа на рис. 2 представлены устройства, структурные блоки, логические блоки, элементы интерфейса.

 Для формализации логики распределения каждому элементу  интерфейса сопоставим атрибуты :  – идентификатор элемента в виде строки;  – тип элемента, например изображение, видеоматериал, текст, кнопка и т.д. (представлен строкой с названием типа);  – размеры элемента в пикселях в виде пары чисел (ширина и высота);  – координаты центра элемента по горизонтали и вертикали на странице интерфейса (представлены соответствующей парой чисел);  – бинарный признак активности элемента (1 – активен, 0 – не активен);  – идентификатор структурного блока, в котором находится элемент, в виде строки;  – описание логических связей с другими элементами интерфейса в виде множества идентификаторов соответствующих элементов;  – бинарный признак типа контента (1 – основной контент, 0 – второстепенный контент);  – атрибут условия распределения (представлен совокупностью пар «параметр устройства, область допустимых значений параметра»);  – атрибут пользовательских предпочтений (представлен совокупностью пар «параметр устройства, область допустимых значений параметра»);  – бинарный признак конфиденциальности элемента (1 – конфиденциальный, 0 – не содержит конфиденциальных данных);   – требования к параметрам устройства, при удовлетворении которых элемент может быть распределен на это устройство (представлены совокупностью пар «параметр устройства, область допустимых значений параметра»).

Каждому устройству  сопоставим параметры : - тип устройства в виде строки с его названием;  – размер диагонали дисплея устройства в виде соответствующего числа; – бинарный параметр мобильности (1 – устройство является мобильным, 0 – не является);  - операционная система устройства в виде строки с соответствующим названием;  – бинарный параметр наличия динамиков (1 - устройство воспроизводит звук, 0 – не воспроизводит). Требованиями к устройству  назовем совокупность допустимых значений параметров  устройства . Факт удовлетворения устройства  требованиям  обозначим как . Факт соответствия требований    атрибутам  элемента  интерфейса обозначим как .

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

Сформулируем правила распределения с использованием введенных обозначений.

1.1. Правило основного устройства основано на том, что пользователи делят все устройства на два типа: устройство для интерфейса основной задачи и остальные устройства для поддержки ее выполнения [7]. В соответствии с этим правилом для интерфейса основной задачи выбирается устройство, которое должно обеспечивать наилучшее взаимодействие пользователя с приложением, т.е. в любом наборе устройств  существует одно основное устройство .

1.2. Правило логической связности основано на делении элементов интерфейса на связные логические группы [8]. В соответствии с этим правилом разбиение такой группы при распределении не допускается, т.е. распределение логической группы на какое-либо устройство должно происходить целиком, или, формально: если у какого-либо элемента атрибут , где  - элементы, входящие в одну логическую группу, то , где  - устройство, на которое распределяются все эти элементы.

1.3. Правило устоявшихся условностей основано на учете при распределении элементов интерфейса множества сформировавшихся за последние годы устоявшихся условностей [9]. К таким условностям, в частности, относятся: распределение интерфейса управления воспроизведением видеоконтента на вспомогательные мобильные устройства [7; 10]; распределение элементов интерфейса, которые используют геолокацию, на мобильные устройства. Запишем это правило формально: если  и доступно устройство , такое, что , то .

1.4. Правило учета пользовательских предпочтений основано на том факте, что пользователи предпочитают некоторые устройства для выполнения определенных задач, несмотря на возникающие при этом неудобства. К таким предпочтениям, в частности, относятся: использование смартфона для проверки электронной почты и обмена сообщениями в мессенджерах, несмотря на неудобство ввода текста на таких устройствах; распределение элемента интерфейса прослушивания музыки на вспомогательное мобильное устройство [11]. Следовательно, при распределении элемента интерфейса необходимо учитывать такие предпочтения. Запишем это правило формально: если  и доступно устройство , такое, что , то .

1.5. Правило конфиденциальности предусматривает, что элемент интерфейса для ввода персональных данных следует распределять на мобильное устройство, поскольку вероятность кражи введенной конфиденциальной информации на мобильном устройстве ниже, чем на персональных компьютерах и ноутбуках.  Запишем это правило формально: если  и доступно устройство , такое, что , то .

1.6. Правило ограничения распределения предусматривает, что устройство пригодно для распределения элементов интерфейса при условии, что оно поддерживает эти элементы и соответствует им с точки зрения удобства [6]. Например, устройства Apple не поддерживают Flash-видео. Хотя разработчики браузеров нашли соответствующее решение для этих устройств, воспроизведение файлов большого объема происходит с задержками. Запишем это правило формально: если  и доступно устройство , такое, что , то .

1.7. Правило второстепенных элементов предусматривает, что второстепенные элементы интерфейса распределяются на вспомогательные устройства. Распределение второстепенных элементов на вспомогательное устройство позволяет уменьшить высоту прокрутки страницы, что увеличит вероятность просмотра всей страницы [12]. Запишем это правило формально: если  и доступно устройство , такое, что ,  то .

Атрибуты элементов интерфейса могут удовлетворять нескольким правилам одновременно. Тогда встает вопрос, в соответствии с каким правилом выполнять распределение. Для этого введем дополнительные правила.

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

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

1.10. Правило превосходства пользовательских предпочтений над конфиденциальностью предусматривает приоритет правила 1.4 над правилом 1.5. Другими словами, если атрибуты объекта удовлетворяют правилу 1.4, то правило 1.5 не применяется. Введение этого правила обусловлено приоритетом пожеланий пользователя над требованиями безопасности. Впрочем, в некоторых случаях это правило может быть заменено на свою противоположность (превосходство конфиденциальности над пользовательскими предпочтениями), например в военном ПО.

2. Процедура распределения элементов интерфейса

Для распределения интерфейса в соответствии с приведенными правилами применяется процедура, состоящая из 6 шагов:

Шаг 1. Задать экспертным путем атрибуты элементов  интерфейса.

Шаг 2. Определить основное устройство  в соответствии с правилом 1.1.

Шаг 3. Распределить элементы интерфейса в соответствии с правилами 1.2, 1.3 и 1.4.

Шаг 4. Распределить оставшиеся нераспределенными после шага 3 элементы интерфейса, представляющие собой левую и/или правую колонки, в соответствии с правилами 1.2, 1.5, 1.6.

Шаг 5. Распределить оставшиеся нераспределенными после шага 4 элементы интерфейса основного блока в соответствии с правилами 1.2, 1.6, 1.7.

Шаг 6. Распределить оставшиеся нераспределенными после шага 5 элементы интерфейса, представляющие собой логические блоки левой и/или правой колонок, в соответствии с правилами 1.2, 1.6.

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

3. Верификация распределения элементов интерфейса на основе пи-исчисления

Пи-исчисление было предложено в конце 1980-х годов Милнером [13] для моделирования взаимодействующих систем, процессы в которых имеют изменяющуюся структуру. К таким системам относятся распределенные интерфейсы.

Коммуникация процессов формально описывается с помощью аксиомы редукции:

где ,  – процессы;  – канал связи;  и  – сообщения; выражение  означает терм, получающийся из терма процесса  символьной подстановкой  вместо .

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

Для управления распределением вводится процесс , внутренним действием  которого является выполнение процедуры распределения. Процесс  имеет каналы связи со всеми процессами, которые представляют устройства, а конкретно с  и , как показано на рис. 3.

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

Процессы  и  получают сообщение  по каналам , затем отправляют его всем процессам, с которыми они имеют связь, кроме процесса . Процесс  одновременно отправляет сообщение  процессам  по каналам . Процессы  и  имеют следующее описание в терминах пи-исчисления на данном шаге:

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

                                                     

 

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

Шаг 2. Выполняется определение основного устройства . Для этого процесс  одновременно передает сообщение  с запросом параметров  по каналам  . Далее процесс ожидает ответы   с параметрами от процессов  и  . Процесс  в терминах пи-исчисления на данном шаге описывается выражением

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

После получения множеств параметров  и  от процессов  и    процесс определяет основное устройство  и формирует набор устройств .

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

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

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

Применим аксиому (1) для процессов  и , тогда описание этих процессов в терминах пи-исчисления будет иметь вид

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

Шаги 5 и 6. Распределение элементов основного блока  в соответствии с правилами 1.2, 1.6, 1.7 и распределение логических блоков левой  и/или правой  колонок в соответствии с правилами 1.2, 1.6 пропускаются, так как набор устройств  уже не содержит свободных вспомогательных устройств.

На рис. 4 представлен граф интерфейса после взаимодействий между процессами.

Для верификации распределения был использован инструмент PiVizTool [14]. Входными данными при этом служили описания процессов в терминах пи-исчисления (2-23). Результаты верификации показали корректность распределения: после выполнения процедуры произошло корректное переопределение связей между процессами без потери элементов интерфейса.

Заключение           

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

References

1. Elmqvist, N. Distributed user interfaces: State of the art / N. Elmqvist // Distributed User Interfaces. - London: Springer, 2011. - R. 1-12.

2. Sakulin, S.A. Optimizaciya interfeysov veb-stranic s ispol'zovaniem inspirirovannyh prirodoy algoritmov / S.A. Sakulin, A.N. Alfimcev, D.V. Solov'ev, D.A. Sokolov // Vestnik komp'yuternyh i informacionnyh tehnologiy. - 2018. - T. 165. - № 3. - S. 3-10.

3. Il'in, N.I. Situacionnye centry. Opyt, sostoyanie, tendencii razvitiya / N.I. Il'in, N.N. Demidov, E.V. Novikova. - M.: MediaPress, 2011.

4. Bashlykov, A.A. Principy formirovaniya trebovaniy k cheloveko-mashinnomu interfeysu dlya sistem dispetcherskogo kontrolya i upravleniya truboprovodnymi sistemami / A.A. Bashlykov //Avtomatizaciya, telemehanizaciya i svyaz' v neftyanoy promyshlennosti. - 2014. - № 3. - S. 3-10.

5. Zacarinnyy, A.A. Ob ergonomicheskih zavisimostyah mezhdu parametrami situacionnogo zala s ispol'zovaniem izognutogo ekrana / A.A. Zacarinnyy, K.G. Chuprakov // Informatika i ee primeneniya. - 2014. - T. 8. - № 4. - S. 85.

6. Felke-Morris, T. Web Development and Design Foundations with HTML5 / Terry Felke-Morris. - 2016.

7. Yang, J. Panelrama: enabling easy specification of cross-device web applications / J. Yang, D. Wigdor // Proceedings of the SIGCHI Conference on Human Factors in Computing Systems. - ACM, 2014. - R. 2783-2792.

8. Pribeanu, C. A Revised Set of Usability Heuristics for the Evaluation of Interactive Systems / C. Pribeanu // Informatica Economica. - 2017. - T. 21. - № 3. - R. 31.

9. Krug, S. Don't make me think: Web & Mobile Usability: Das intuitive Web / S. Krug. - MITP-Verlags GmbH & Co. KG, 2018.

10. Fisher, E.R. Designing the Distributed User Interface: Case Studies on Building Distributed Applications / E.R. Fisher, S.K. Badam, N. Elmqvist // Preprint submitted to International Journal of Human-Computer Interaction. - 2013. - February 15.

11. Nebeling, M. Xdbrowser: User-defined cross-device web page designs / M. Nebeling, A.K. Dey // Proceedings of the 2016 CHI Conference on Human Factors in Computing Systems. - ACM, 2016. - R. 5494-5505.

12. Qiu, X. Limited individual attention and online virality of low-quality information / X. Qiu [et al.] // Nature Human Behaviour. - 2017. - T. 1. - № 7. - R. 132.

13. Milner, R. Communicating and mobile systems: the pi calculus / R. Milner. - Cambridge university press, 1999.

14. Papapanagiotou, P. Formal verification approach to process modelling and composition / P. Papapanagiotou. - 2014.

Login or Create
* Forgot password?