Sammanfattning av denna webbsida: Denna artikel presenterar de centrala begreppen för PLC-statecharts - en anpassning av UML-statecharts som kan användas som ett visuellt programmeringsspråk för PLCs. De kombinerar fördelarna med UMLstatecharts med en strikt formell grund och kan öppet användas inom ramen för IEC 61131-3 (3 rd Edition). De definierade formella beteendesemantik sätter grunden för en automatisk omvandling av PLC-statecharts till tidsinställda automata som kan analyseras av modellen-checker UPPAAL. Detta arbete utgör en aspekt av större verk Vogel-Heuser 2009, Witsch et. al 2010) som syftar till att integrera en delmängd av de diagram som definieras i Unified Modeling Language (UML) (OMG 2009) och IEC 61131-3 (IEC 2010) för att underlätta programvaruutveckling för PLC. Detta arbete motiveras av att programvaruutveckling i samband med automationssystem blir alltmer komplex och rör sig mot modellbaserade utvecklingsmetoder eller åtminstone mot programmeringskoncept som erbjuder en högre abstraktionsnivå. Det kommer dock att bli nödvändigt att integrera dagens IEC 61131-3 arvskod på ett öppet sätt. Med tanke på den mänskliga faktorn behöver tekniker välutbildade i IEC 61131-3 också kunna programmera PLCs på det konventionella sättet (vilket erbjuder en komplett ny programmeringsstrategi är inte en lösning). Å andra sidan används nästa generation av PLC-programmerare för att modellera språk som UML. Eftersom dessa grupper måste samarbeta i samma projekt föreslår vi att begrepp som statskort integreras i klassiska IEC 61131-3-miljöer. Omgivningsarbeten handlar om den dubbelriktade kartläggningen av UML-klassdiagram och IEC 61131-3, 3 rd-utgåvan som sannolikt kommer med objektorienterade förlängningar. Ytterligare UML-aktivitet diagram, som inför petri-net som semantik i UML (OMG 2009, s. 324) är en del av de större verk och står bredvid PLC-statecharts delvis beskrivs i detta papper. Eftersom vi också implementerar ett petri-net liknande beteende med aktivitet diagram vi begränsar vår hänsyn till befintliga metoder i detta papper för att ange maskiner och inte titta på petri-nät som beaktas av Frey (Frey 2002). Eftersom PLC-tillämpningar i allmänhet ställer höga krav på programvaras kvalitet (dvs. korrekthet, robusthet) överväger vi formella specifikations- och analystekniker i detta arbete. Dessa tekniker gör det till exempel möjligt att formellt bevisa kritiska egenskaper. För att kort sammanfatta, presenterar detta dokument N en anpassning av UML state-charts tillägnad för integrationen i IEC 61131-3 (PLC-statecharts) med en formell syntax, N en formellt definierad beteende semantik genom att kartlägga PLC-statechart element till motsvarande tidsinställda automatiserade konstruktioner för modell-checker UPPAAL. N Genom detta kan tillämpningen av PLC-statecharts enkelt stödja kodsyntes, men också formella metoder som modellkontroll. Därefter ger vi en kort introduktion till modellkontroll och diskuterar befintliga arbeten om statskort i samband med PLC. Modellkontroll är en formell, uttömmande modellanalysteknik som kan ge otvetydiga resultat. Denna teknik kräver att specifikationen av systemet och de egenskaper som ska kontrolleras definieras. Modellkontrollören returnerar om systemet uppfyller dessa egenskaper i alla möjliga fall eller inte. Om systemet bryter mot de angivna egenskaperna returnerar modellkontrollen ett felspår. På grund av den så kallade stat space-explosion problem modellkontroll är starkt begränsad när det gäller modellens komplexitet. Men flera verk som Hendriks och Larsen, Giese et. Al, Witsch m.fl. visa hur man utformar komplexa modeller som kan beräknas effektivt, så att modellkontroll kan tillämpas framgångsrikt i relevanta modeller. Utan förlust av allmängiltighet kommer vi att använda modeller för modellkontroll som skapats i UPPAAL-verktygsetet för att definiera en exekverbar, beteendemässig formell semantik av PLC-statecharts i detta arbete. UPPAAL är en integrerad verktygsuppsättning för modellering, simulering och verifiering av tidsinställda system. Den tillhör den tidsinställda, symboliska modellkontrollören och använder tidsinställd automata (Alur och Dill, 1990) för modelleringsändamål. För att öka läsbarheten av detta papper, kommer en kort introduktion till UPAAL automata att ges senare. En detaljerad introduktion till UPPAAL ges av Behrmann, et al.. UPPAAL automata består av platser (cirklar) och kanter, var och en ansluter två av dem.
Vogel-Heuser m.fl. REF presenterar de centrala begreppen för PLCstatecharts - en anpassning av UML-statecharts - som kan användas som ett visuellt programmeringsspråk för PLCs.
PLC-Statecharts: An Approach to Integrate UML-Statecharts in Open-Loop Control Engineering-Aspects on Behavioral Semantics and Model-Checking
{'venue': None, 'journal': 'IFAC Proceedings Volumes', 'mag_field_of_study': ['Computer Science']}