آموزش مدل‌سازی رسمی کمی و تحلیل عملکرد در بدترین حالت - آخرین آپدیت

سرفصل ها و درس ها

مقدمه Introduction

• مقدمه Introduction

مدل‌سازی سیستم‌ها به عنوان سیستم‌های تولید/مصرف توکن Modeling systems as token consumption/production systems

• یک تصویر گویاتر از هزار کلمه است A single picture tells more than a thousand words

• مصرف و تولید توکن‌ها Consumption and production of tokens

• مدل‌سازی واحد مراقبت‌های ویژه Modeling an intensive care unit

• مدل‌سازی رادیوی شبکه محلی بی‌سیم (WLAN) Modeling a wireless LAN radio

• مدل‌سازی و اصلاح یک ربات صنعتی Modeling and refining an industrial robot

• سیستم خود را انتخاب کنید Pick your own system

• انواع شبکه‌های پتری Classes of Petri-nets

• علیت، انتخاب و هم‌روندی (الگوهای مدل‌سازی) Causality, choice and concurrency (modeling patterns)

• اصلاح سیستم‌های مصرف/تولید Refinement of consumption/production systems

• تفسیر تصاویر برای تحلیل عملکرد Interpreting pictures for performance analysis

• مدل خود را رسم کنید Draw your own model

سینتکس و معناشناسی Syntax and semantics

• هشدار: خود را برای نظریه مجموعه‌ها آماده کنید! Warning: prepare for some set theory!

• سینتکس و معناشناسی Syntax and semantics

• مبانی و اصول The basics

• توسعه‌ها Extensions

• ترتیب‌های پیشوندی Prefix orders

• تمرین در مورد ترتیب‌های پیشوندی Exercise on prefix orders

• اثبات اینکه جریان‌ها یک ترتیب پیشوندی تشکیل می‌دهند Proof that flows form a prefix order

• فرموله کردن تفسیرها به عنوان تابع Formalizing interpretations as functions

• شمارش، حفظ‌کننده ترتیب است Counting is order preserving

• فرموله کردن تفسیر شبکه پتری Formalizing the Petri-net interpretation

• اثبات اینکه تعداد توکن‌ها در یک چرخه جریان داده تک‌نرخی ثابت است Proof that the number of tokens in a single-rate dataflow cycle is constant

• فرموله کردن زمان‌بندی Formalizing timing

• فرموله کردن زمان‌بندی مشتاقانه (Eager Scheduling) Formalizing eager scheduling

• فرموله کردن زمان‌بندی دوره‌ای Formalizing periodic scheduling

تحلیل عملکرد Performance analysis

• مثال جاری Running example

• نرخ عبور توسط 1/MCM محدود می‌شود Throughput is bounded by 1/MCM

• اثبات الف Proof - a

• اثبات ب Proof - b

• اثبات ج Proof - c

• اثبات د Proof - d

• اثبات ه Proof - e

• اثبات و Proof - f

• اثبات ز Proof - g

• اثبات ح Proof - h

• اثبات ط Proof - i

• اثبات ی Proof - j

• کران نرخ عبور دقیق است The throughput bound is tight

• زمان‌بندی دوره‌ای یک گراف جریان داده Periodic scheduling of a dataflow graph

• تحلیل تأخیر در یک زمان‌بندی دوره‌ای Latency analysis of a periodic schedule

• تحلیل تأخیر در یک زمان‌بندی مشتاقانه Latency analysis of an eager schedule

• تعریف رسمی تأخیر The formal definition of latency

• زمان راه‌اندازی (Boot up) یک گراف جریان داده The boot-up time of a dataflow graph

• بهینه‌سازی تخمین‌های تأخیر نسبت به زمان راه‌اندازی Optimizing latency estimates w.r.t. boot-up time

• بافترینگ و فشار معکوس (Backpressure) Buffering and backpressure

یک مثال نهایی One final example

• یک مثال نهایی One final example