Инсерционное моделирование А.Летичевский Семинар «Образный компьютер» 10 Мая 2011

Содержание Инсерционное моделирование Математические основания Инсерционные машины Базовые протоколы Верификация в системе VRS Май Образный компьютер2

Май Инсерционное моделирование: Технология построения и исследования моделей многокомпонентных распределенных систем, представленных с помощью композиции агентов и сред Формально Агенты и среды: Атрибутные транзиционные системы Композиция: непрерывная функция погружения, характеризующая изменение поведения среды в результате погружения агента Образный компьютер

Май Образный компьютер4 Исторические замечания Идея «Взаимодействия агентов и сред» появилась в 1996 году в результате совместных исследований с Д.Гильбертом в Сити Университете в Лондоне. С 2000 она использовалась при разработке средств верификации требований краспределенным программным системам. Реализована в системе VRS, разработанной по заказу Моторолы. В настоящее время используется компанией Uniquesoft для создания новых средств разработки программных cистем. Одновременно в ИК разрабатывается система инсерционного моделирования IMS

Insertion modeling paradigm Май Образный компьютер agent environment agent environment Insertion function The world is a hierarchy of environments and agents inserted into them. Environments and agents are entities evolving in time. Insertion of agent into environment changes the behavior of environment and produces new environment which is ready for insertion of new agents (if there is a room). Environments as agents can be inserted into higher level environment. Agents can be inserted from external environment as well as from internal agents (environments). Agents and environments can model another agents and environments on the different levels of abstraction

Май Образный компьютер6 Mathematical foundations Transition systems Agents Behaviors and behavior algebras Environments and insertion function Insertion equivalence of agents Process algebras

a Transition systems Май Образный компьютер Agents and environments are labeled or attributed transition systems considered up to bisimilarity (bisimilar states have the same behavior that is cannot be distinguished by an observer). b a b b b a a a a b b aa a a a a b b b

8 s s's' Поведение транзиционной системы: множество последовательностей действий, которые она может совершить (?) Май Образный компьютер

9 Бисимуляционная эквивалентность bisimilarity (Milner 1980, D.Park 1981) Отношение бисимуляции (bisimulation): a R s a t R a R s a t R bisimulation => bisimilarity (бисимуляционная эквивалентность) Май Образный компьютер

Май Образный компьютер10 Agents x y:Δ a aa b a Δ x:(a.0)+a.(b.(y:(a.0+a. Δ + Δ)) + bot) Attribued transition systems with divergence and terminal states considered up to bisimularity. Behaviors Elements of continuous complete behaviour algebra F(A) over a set of actions A (a kind of process algebra). Extensions: functions defined by recursive definitions in F(A) Sates as behaviors.

Май Образный компьютер11 Environments and insertion functions Insertion function must be continuous n Insertion of several agents Multilevel insertion is a complete behavior algebra over action algebra (a kind of process algebra).

Май Образный компьютер12 Insertion equivalence Semigroup of environment transformations Equivalence

Май Образный компьютер13 Traditional algebras of communicating processes (CCS, CSP, ACP, π-calculus,...) can be obtained by selection of an environment and its insertion function.

Май Образный компьютер14 One-step insertion Classification of insertion functions Look-ahead insertion (прогнозирующее погружение) continuous Head insertion (префиксное погружение) continuous

Май Образный компьютер15 Insertion machines: implementation of insertion models Real time insertion machines Analytical insertion machines

Real time insertion machine Май Образный компьютер 16 Agent behavior unfolder Environment interactor Model driver Input model Unfolding recursive definitions Computing insertion function and making nondeterministic choice External environment External insertion function

Analytical insertion machine Май Образный компьютер 17 Agent behavior unfolder Environment interactor Model driver Input model Goal state Filters Search control Unfolding recursive definitions Computing insertion function Output traces

Май Образный компьютер18 IMS is an environment for the development of insertion machines (new project of Glushkov Institute of Cybernetics)

Some insertion machines developed previously Май Образный компьютер19 Semantics of MSC (2002, 2005) Glushkov evidence algorithm (2002, 2003) Semantics of Basic Protocols (2005) Trace Generators for VRS (2008) Checking security protocols (2009) Creatures and substance (2009) Proving program correctness and generating invariants

BPSL Basic Protocol Specification Language used in VRS Май Образный компьютер20

21 Basic protocol Precondition Properties of environment First order quantifier with typed variables Postcondition Finite process (behavior) of attributed environment with inserted agents Environment property Combination of Hoar triples with the model of interaction of agents and environments. A method to define insertion function (look-ahead) by representing its local properties. Май Образный компьютер

BPSL implemented in VRS environment description + set of BPs Май Образный компьютер22 Types: Data types simple: int, real, Bool, enumerated, symbolic (free terms), agent behaviors (process algebra) lists: list of τ (simple) functional: (simple, arrays are considered as functional types with restrictions on the domains of indexes) Agent types: defined by the set of typed agent attributes Agent behaviors: defined by recursive equations Environment attributes: used as functional symbols (simple= arity 0) Agent attributes: typed names

Preconditions and postconditions Май Образный компьютер23 Environment description defines a signature of multisorted algebra and domains for types (sorts). Precondition is a first order formula over signature defined by environment description. Postcondition is a formula + assignments + update operators for lists. Assignments and updates are considered as a temporal logic formula. Formulas for lists: u=(t1,t2,…) or Exist x(u=p*x*q). Existential quantifiers are allowed in formulas.

VRS tools Concrete Trace Generator (CTG) Symbolic Trace Generator (STG) Static Requirements Checker (SRC) Май Образный компьютер24

Concrete trace generator analytical insertion machine for concrete models Май Образный компьютер All attributes have concrete values in the state of environment and agents states. Each instantiated basic protocol defines single- valued transformation of environment state: Analog: model checker for BP-specifications Goal state, safety conditions Filters and search control, LTL, Symmetry, dynamic abstraction,…

Май Образный компьютер Symbolic trace generator analytical insertion machine for concrete models Possible values of environment and agent attributes are defined by means of logic formulas. Transition rules defined by means of corresponding deductive system Predicate transformer computes the strongest postcondition.

Май Образный компьютер Static requirement checker algorithms based on predicate transformer Proving properties of requirements without generating traces. Completeness Consistency Safety Reachability (reduced to safety)

Май Образный компьютер Future development of IMS Models, defined by local properties (generalization of basic protocols) Proving correctness of programs Solving constraint problems Developing new cognitive architecture on a base of IMS